deffunc H₁( Nat, set ) -> Element of NAT = 5 + ($1 + 1);
consider f being Function of NAT ,NAT such that
A1: ( f . 0 = 5 + 0 & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) from NAT_1:sch 12();

A2: now

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 & proj1 g = NAT & proj2 g = VAR )
thus g is one-to-one :: thesis: ( proj1 g = NAT & proj2 g = VAR )

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 g or not b₁ in proj1 g or not g . x = g . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 g or not y in proj1 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: proj2 g = VAR
thus rng g c= VAR :: according to XBOOLE_0:def 10 :: thesis: VAR c= proj2 g

proof

let x be set ; :: 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 set such that
A4: y in dom f and
A5: x = f . y by FUNCT_1:def 5;
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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in VAR or x in proj2 g )
assume x in VAR ; :: thesis: x in proj2 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 13;
then f . n = x by A2, A7;
hence x in proj2 g by A3, A8, FUNCT_1:def 5; :: thesis: verum

end;