[: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_{1}( 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_{1}(n,m)
from BINOP_1:sch 4();

A3: f is one-to-one

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

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

consider f being Function of [:NAT,NAT:],NAT such that

A2: for n, m being Element of NAT holds f . (n,m) = H

A3: f is one-to-one

proof

( dom f = [:NAT,NAT:] & rng f c= NAT )
by FUNCT_2:def 1;
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;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

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