set f = the Enumeration of A;
( dom the Enumeration of A = A & rng the Enumeration of A c= NAT ) by AOFA_I00:6, AOFA_I00:11;
then the Enumeration of A is Function of A,NAT by FUNCT_2:2;
hence ex b₁ being Function of A,NAT st b₁ is one-to-one ; :: thesis: verum