deffunc H₁( object ) -> object = [0,$1];
consider f being Function such that
A1: dom f = NAT and
A2: for x being object st x in NAT holds
f . x = H₁(x) from FUNCT_1:sch 3();
A3: f is one-to-one

proof

now :: thesis: for x, y being object st x in dom f & y in dom f & f . x = f . y holds
x = y

let x, y be object ; :: thesis: ( x in dom f & y in dom f & f . x = f . y implies x = y )
assume that
A4: x in dom f and
A5: y in dom f and
A6: f . x = f . y ; :: thesis: x = y
f . y = [0,y] by A5, A1, A2;
then [0,x] = [0,y] by A6, A4, A1, A2;
hence x = y by XTUPLE_0:1; :: thesis: verum

end;

hence f is one-to-one by FUNCT_1:def 4; :: thesis: verum

end;

rng f = { [0,n] where n is Nat : verum }

proof

A7: rng f c= { [0,n] where n is Nat : verum }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in { [0,n] where n is Nat : verum } )
assume x in rng f ; :: thesis: x in { [0,n] where n is Nat : verum }
then consider y being object such that
A8: y in dom f and
A9: x = f . y by FUNCT_1:def 3;
reconsider z = y as Nat by A8, A1;
x = [0,z] by A9, A2, A1, A8;
hence x in { [0,n] where n is Nat : verum } ; :: thesis: verum

end;

{ [0,n] where n is Nat : verum } c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [0,n] where n is Nat : verum } or x in rng f )
assume x in { [0,n] where n is Nat : verum } ; :: thesis: x in rng f
then consider n being Nat such that
A10: x = [0,n] ;
( n in dom f & f . n = [0,n] ) by A1, A2, ORDINAL1:def 12;
hence x in rng f by A10, FUNCT_1:3; :: thesis: verum

end;

hence rng f = { [0,n] where n is Nat : verum } by A7; :: thesis: verum

end;

hence { [0,n] where n is Nat : verum } is infinite by A1, A3, CARD_1:59; :: thesis: verum