defpred S₁[ object , object ] means ex g0 being sequence of the carrier of G ex h being Element of G st
( $1 = h & g0 = $2 & g0 . 0 = 0_ G & ( for n being Nat holds g0 . (n + 1) = (g0 . n) + h ) );
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 = $2 + b;
consider g0 being sequence of the carrier of G such that
A2: g0 . 0 = 0_ G and
A3: for n being Nat holds g0 . (n + 1) = H₁(n,g0 . n) from NAT_1:sch 12();
reconsider y = g0 as set ;
take y ; :: thesis: S₁[x,y]
take g0 ; :: thesis: ex h being Element of G st
( x = h & g0 = y & g0 . 0 = 0_ G & ( for n being Nat holds g0 . (n + 1) = (g0 . n) + h ) )
take b ; :: thesis: ( x = b & g0 = y & g0 . 0 = 0_ G & ( for n being Nat holds g0 . (n + 1) = (g0 . n) + b ) )
thus ( x = b & g0 = y & g0 . 0 = 0_ G ) by A2; :: thesis: for n being Nat holds g0 . (n + 1) = (g0 . n) + b
let n be Nat; :: thesis: g0 . (n + 1) = (g0 . n) + b
thus g0 . (n + 1) = (g0 . n) + b by A3; :: thesis: verum

end;

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

proof

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

end;

consider F being Function of [:NAT, the carrier of G:], the carrier of G such that
A7: for n being Nat
for a being Element of G holds S₂[n,a,F . (n,a)] from GROUP_1A:sch 1(A5);
take F ; :: thesis: for h being Element of G holds
( F . (0,h) = 0_ G & ( for n being Nat holds F . ((n + 1),h) = (F . (n,h)) + h ) )
let h be Element of G; :: thesis: ( F . (0,h) = 0_ G & ( for n being Nat holds F . ((n + 1),h) = (F . (n,h)) + h ) )
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) = (g2 . n) + b ) ) by A4;
ex g1 being sequence of the carrier of G st
( g1 = f . h & F . (0,h) = g1 . 0 ) by A7;
hence F . (0,h) = 0_ G by A8; :: thesis: for n being Nat holds F . ((n + 1),h) = (F . (n,h)) + h
let n be Nat; :: thesis: F . ((n + 1),h) = (F . (n,h)) + h
A9: 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) = (g2 . n) + b ) ) by A4;
( ex g0 being sequence of the carrier of G st
( g0 = f . h & F . (n,h) = g0 . n ) & ex g1 being sequence of the carrier of G st
( g1 = f . h & F . ((n + 1),h) = g1 . (n + 1) ) ) by A7;
hence F . ((n + 1),h) = (F . (n,h)) + h by A9; :: thesis: verum