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

proof

let x be set ; :: thesis: ( x in the carrier of G implies ex y being set st S₁[x,y] )
assume x in the carrier of G ; :: thesis: ex y being set 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 Function of NAT ,the carrier of G such that
A13: ( 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 Element of NAT holds g0 . (n + 1) = x \ ((g0 . n) ` ) ) )
take b ; :: thesis: ( x = b & g0 = y & g0 . 0 = 0. G & ( for n being Element of NAT holds g0 . (n + 1) = b \ ((g0 . n) ` ) ) )
thus ( x = b & g0 = y & g0 . 0 = 0. G ) by A13; :: thesis: for n being Element of NAT holds g0 . (n + 1) = b \ ((g0 . n) ` )
let n be Element of NAT ; :: thesis: g0 . (n + 1) = b \ ((g0 . n) ` )
thus g0 . (n + 1) = b \ ((g0 . n) ` ) by A13; :: thesis: verum

end;

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

proof

let a be Element of G; :: thesis: for n being Element of NAT ex b being Element of G st S₂[a,n,b]
let n be Element of NAT ; :: thesis: ex b being Element of G st S₂[a,n,b]
consider g0 being Function of NAT ,the carrier of G, h being Element of G such that
a = h and
A17: g0 = f . a and
( g0 . 0 = 0. G & ( for n being Element of NAT holds g0 . (n + 1) = h \ ((g0 . n) ` ) ) ) by A15;
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 A17; :: thesis: verum

end;

consider F being Function of [:the carrier of G,NAT :],the carrier of G such that
A18: for a being Element of G
for n being Element of NAT holds S₂[a,n,F . a,n] from BINOP_1:sch 3(A16);
take F ; :: thesis: for x being Element of G holds
( F . x,0 = 0. G & ( for n being Element of 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 Element of NAT holds F . h,(n + 1) = h \ ((F . h,n) ` ) ) )
A19: ex g1 being Function of NAT ,the carrier of G st
( g1 = f . h & F . h,0 = g1 . 0 ) by A18;
ex g2 being Function of NAT ,the carrier of G ex b being Element of G st
( h = b & g2 = f . h & g2 . 0 = 0. G & ( for n being Element of NAT holds g2 . (n + 1) = b \ ((g2 . n) ` ) ) ) by A15;
hence F . h,0 = 0. G by A19; :: thesis: for n being Element of NAT holds F . h,(n + 1) = h \ ((F . h,n) ` )
let n be Element of NAT ; :: thesis: F . h,(n + 1) = h \ ((F . h,n) ` )
A20: ex g0 being Function of NAT ,the carrier of G st
( g0 = f . h & F . h,n = g0 . n ) by A18;
A21: ex g1 being Function of NAT ,the carrier of G st
( g1 = f . h & F . h,(n + 1) = g1 . (n + 1) ) by A18;
consider g2 being Function of NAT ,the carrier of G, b being Element of G such that
A22: ( h = b & g2 = f . h & g2 . 0 = 0. G ) and
A23: for n being Element of NAT holds g2 . (n + 1) = b \ ((g2 . n) ` ) by A15;
thus F . h,(n + 1) = h \ ((F . h,n) ` ) by A20, A21, A22, A23; :: thesis: verum