theorem :: ZF_FUND1:29

for A being finite Subset of VAR holds A, code A are_equipotent by Lm8;