[:NAT,{0}:] c= [:NAT,NAT:] by ZFMISC_1:95;
then card [:NAT,{0}:] c= card [:NAT,NAT:] by CARD_1:11;
then A1: card NAT c= card [:NAT,NAT:] by CARD_1:69;
deffunc H₁( Element of NAT , Element of NAT ) -> Element of omega = (2 |^ $1) * ((2 * $2) + 1);
consider f being Function of [:NAT,NAT:],NAT such that
A2: for n, m being Element of NAT holds f . (n,m) = H₁(n,m) from BINOP_1:sch 4();
A3: f is one-to-one

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume x in dom f ; :: thesis: ( not y in dom f or not f . x = f . y or x = y )
then consider n1, m1 being Element of NAT such that
A4: x = [n1,m1] by Lm2;
assume y in dom f ; :: thesis: ( not f . x = f . y or x = y )
then consider n2, m2 being Element of NAT such that
A5: y = [n2,m2] by Lm2;
assume A6: f . x = f . y ; :: thesis: x = y
A7: (2 |^ n1) * ((2 * m1) + 1) = f . (n1,m1) by A2
.= f . (n2,m2) by A4, A5, A6
.= (2 |^ n2) * ((2 * m2) + 1) by A2 ;
then n1 = n2 by Th4;
hence x = y by A4, A5, A7, Th4; :: thesis: verum

end;

( dom f = [:NAT,NAT:] & rng f c= NAT ) by FUNCT_2:def 1;
then card [:NAT,NAT:] c= card NAT by A3, CARD_1:10;
then card NAT = card [:NAT,NAT:] by A1;
hence ( [:NAT,NAT:], NAT are_equipotent & card NAT = card [:NAT,NAT:] ) by CARD_1:5; :: thesis: verum