Round-six lemma `exNet_OK`