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