let A be finite Subset of VAR; :: thesis: A, code A are_equipotent
A1: ( (decode ") | A is one-to-one & rng ((decode ") | A) = code A ) by Lm1, FUNCT_1:52, RELAT_1:115;
dom ((decode ") | A) = (dom (decode ")) /\ A by RELAT_1:61
.= A by Lm1, XBOOLE_1:28 ;
hence A, code A are_equipotent by A1, WELLORD2:def 4; :: thesis: verum