deffunc H1( Nat, set ) -> Element of omega = 5 + ($1 + 1);
consider f being sequence of NAT such that
A1: ( f . 0 = 5 + 0 & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) from NAT_1:sch 12();
A2: now :: thesis: for n being Element of NAT holds f . n = 5 + n
let n be Element of NAT ; :: thesis: f . n = 5 + n
( ex j being Nat st n = j + 1 implies f . n = 5 + n ) by A1;
then ( n = 0 or f . n = 5 + n ) by NAT_1:6;
hence f . n = 5 + n by A1; :: thesis: verum
end;
A3: dom f = NAT by FUNCT_2:def 1;
thus NAT , VAR are_equipotent :: thesis: verum
proof
reconsider g = f as Function ;
take g ; :: according to WELLORD2:def 4 :: thesis: ( g is one-to-one & dom g = NAT & rng g = VAR )
thus g is one-to-one :: thesis: ( dom g = NAT & rng g = VAR )
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom g or not y in dom g or not g . x = g . y or x = y )
assume ( x in dom g & y in dom g ) ; :: thesis: ( not g . x = g . y or x = y )
then reconsider n1 = x, n2 = y as Element of NAT by FUNCT_2:def 1;
( f . n1 = 5 + n1 & f . n2 = 5 + n2 ) by A2;
hence ( not g . x = g . y or x = y ) by XCMPLX_1:2; :: thesis: verum
end;
thus dom g = NAT by FUNCT_2:def 1; :: thesis: rng g = VAR
thus rng g c= VAR :: according to XBOOLE_0:def 10 :: thesis: VAR c= rng g
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in VAR )
assume x in rng g ; :: thesis: x in VAR
then consider y being object such that
A4: y in dom f and
A5: x = f . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A4;
A6: 5 + y >= 5 by NAT_1:11;
x = 5 + y by A2, A5;
hence x in VAR by A6; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in VAR or x in rng g )
assume x in VAR ; :: thesis: x in rng g
then ex n being Element of NAT st
( x = n & 5 <= n ) ;
then consider n being Nat such that
A7: x = 5 + n by NAT_1:10;
A8: n in NAT by ORDINAL1:def 12;
then f . n = x by A2, A7;
hence x in rng g by A3, A8, FUNCT_1:def 3; :: thesis: verum
end;