deffunc H_{1}( 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_{1}(x)
from FUNCT_1:sch 3();

A3: f is one-to-one

consider f being Function such that

A1: dom f = NAT and

A2: for x being object st x in NAT holds

f . x = H

A3: f is one-to-one

proof

end;

rng f = { [0,n] where n is Nat : verum }
now :: thesis: for x, y being object st x in dom f & y in dom f & f . x = f . y holds

x = y

hence
f is one-to-one
by FUNCT_1:def 4; :: thesis: verumx = 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;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

proof

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

end;proof

{ [0,n] where n is Nat : verum } c= rng f
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;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

proof

hence
rng f = { [0,n] where n is Nat : verum }
by A7; :: thesis: verum
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;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