[:NAT ,{0 }:] c= [:NAT ,NAT :] by ZFMISC_1:118;
then card [:NAT ,{0 }:] c= card [:NAT ,NAT :] by CARD_1:27;
then A1: card NAT c= card [:NAT ,NAT :] by CARD_2:13;
deffunc H₁( Element of NAT , Element of NAT ) -> Element of NAT = (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 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 f or not b₁ in proj1 f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume x in dom f ; :: thesis: ( not y in proj1 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 Th52;
hence x = y by A4, A5, A7, Th52; :: 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:26;
then card NAT = card [:NAT ,NAT :] by A1, XBOOLE_0:def 10;
hence ( [:NAT ,NAT :], NAT are_equipotent & card NAT = card [:NAT ,NAT :] ) by CARD_1:21; :: thesis: verum