[: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 H1( 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) = H1(n,m)
from BINOP_1:sch 4();
A3:
f is one-to-one
proof
let x,
y be
object ;
FUNCT_1:def 4 ( 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
;
( 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
;
( 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
;
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;
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; verum