[::] c= by ZFMISC_1:95;
then card c= card by CARD_1:11;
then A1: card NAT c= card by CARD_1:69;
deffunc H1( Element of NAT , Element of NAT ) -> Element of omega = (2 |^ \$1) * ((2 * \$2) + 1);
consider f being Function of ,NAT such that
A2: for n, m being Element of NAT holds f . (n,m) = H1(n,m) from 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 = & rng f c= NAT ) by FUNCT_2:def 1;
then card c= card NAT by ;
then card NAT = card by A1;
hence ( [::], NAT are_equipotent & card NAT = card ) by CARD_1:5; :: thesis: verum