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 = 1_ 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 = 1_ 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 = 1_ G & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * h ) )
take b ; :: thesis: ( x = b & g0 = y & g0 . 0 = 1_ G & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * b ) )
thus ( x = b & g0 = y & g0 . 0 = 1_ 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₂[ Element of G, Nat, set ] means ex g0 being sequence of the carrier of G st
( g0 = f . $1 & $3 = g0 . $2 );
A5: 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
A6: g0 = f . a and
g0 . 0 = 1_ G and
for n being Nat holds g0 . (n + 1) = (g0 . n) * h by A4;
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 A6; :: thesis: verum

end;

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