Round-six lemma `kFinA_le6`