Round-six lemma `sum_mu`