defpred S₁[ object , object ] means ex f being sequence of the carrier of G ex x being Element of G st
( $1 = x & f = $2 & f . 0 = 0. G & ( for n being Nat holds f . (n + 1) = x \ ((f . n) `) ) );
A1: for x being object st x in the carrier of G holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in the carrier of G implies ex y being object st S₁[x,y] )
assume x in the carrier of G ; :: thesis: ex y being object st S₁[x,y]
then reconsider b = x as Element of G ;
deffunc H₁( Nat, Element of G) -> Element of the carrier of G = b \ ($2 `);
consider g0 being sequence of the carrier of G such that
A2: ( g0 . 0 = 0. G & ( for n being Nat holds g0 . (n + 1) = H<sub>1</sub>(n,g0 . n) ) ) from NAT_1:sch 12();
reconsider y = g0 as set ;
take y ; :: thesis: S<sub>1</sub>[x,y]
take g0 ; :: thesis: ex x being Element of G st
( x = x & g0 = y & g0 . 0 = 0. G & ( for n being Nat holds g0 . (n + 1) = x \ ((g0 . n) `) ) )
take b ; :: thesis: ( x = b & g0 = y & g0 . 0 = 0. G & ( for n being Nat holds g0 . (n + 1) = b \ ((g0 . n) `) ) )
thus ( x = b & g0 = y & g0 . 0 = 0. G & ( for n being Nat holds g0 . (n + 1) = b \ ((g0 . n) `) ) ) by A2; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = the carrier of G & ( for x being object st x in the carrier of G holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A1);
defpred S₂[ Element of G, Nat, set ] means ex g0 being sequence of the carrier of G st
( g0 = f . $1 & $3 = g0 . $2 );
A4: for a being Element of G
for n being Nat ex b being Element of G st S₂[a,n,b]

proof

let a be Element of G; :: thesis: for n being Nat ex b being Element of G st S₂[a,n,b]
let n be Nat; :: thesis: ex b being Element of G st S₂[a,n,b]
consider g0 being sequence of the carrier of G, h being Element of G such that
a = h and
A5: g0 = f . a and
g0 . 0 = 0. G and
for n being Nat holds g0 . (n + 1) = h \ ((g0 . n) `) by A3;
take g0 . n ; :: thesis: S₂[a,n,g0 . n]
take g0 ; :: thesis: ( g0 = f . a & g0 . n = g0 . n )
thus ( g0 = f . a & g0 . n = g0 . n ) by A5; :: thesis: verum

end;

consider F being Function of [: the carrier of G,NAT:], the carrier of G such that
A6: for a being Element of G
for n being Nat holds S₂[a,n,F . (a,n)] from NAT_1:sch 19(A4);
take F ; :: thesis: for x being Element of G holds
( F . (x,0) = 0. G & ( for n being Nat holds F . (x,(n + 1)) = x \ ((F . (x,n)) `) ) )
let h be Element of G; :: thesis: ( F . (h,0) = 0. G & ( for n being Nat holds F . (h,(n + 1)) = h \ ((F . (h,n)) `) ) )
A7: ex g2 being sequence of the carrier of G ex b being Element of G st
( h = b & g2 = f . h & g2 . 0 = 0. G & ( for n being Nat holds g2 . (n + 1) = b \ ((g2 . n) `) ) ) by A3;
ex g1 being sequence of the carrier of G st
( g1 = f . h & F . (h,0) = g1 . 0 ) by A6;
hence F . (h,0) = 0. G by A7; :: thesis: for n being Nat holds F . (h,(n + 1)) = h \ ((F . (h,n)) `)
let n be Nat; :: thesis: F . (h,(n + 1)) = h \ ((F . (h,n)) `)
A8: ex g2 being sequence of the carrier of G ex b being Element of G st
( h = b & g2 = f . h & g2 . 0 = 0. G & ( for n being Nat holds g2 . (n + 1) = b \ ((g2 . n) `) ) ) by A3;
( ex g0 being sequence of the carrier of G st
( g0 = f . h & F . (h,n) = g0 . n ) & ex g1 being sequence of the carrier of G st
( g1 = f . h & F . (h,(n + 1)) = g1 . (n + 1) ) ) by A6;
hence F . (h,(n + 1)) = h \ ((F . (h,n)) `) by A8; :: thesis: verum