Round-six lemma `l13U_arith`