Round-six lemma `dot_body`