deffunc H1( 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 = H1(x) from 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 ;
hence x in rng f by ; :: 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 ; :: thesis: verum