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

proof

let x be object ; :: thesis: ( x in the carrier of X implies ex y being object st S₁[x,y] )
assume x in the carrier of X ; :: thesis: ex y being object st S₁[x,y]
then reconsider b = x as Element of X ;
deffunc H₁( Nat, Element of X) -> Element of X = $2 * b;
consider g0 being sequence of the carrier of X such that
A2: g0 . 0 = 0. X 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 X st
( x = h & g0 = y & g0 . 0 = 0. X & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * h ) )
take b ; :: thesis: ( x = b & g0 = y & g0 . 0 = 0. X & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * b ) )
thus ( x = b & g0 = y & g0 . 0 = 0. X ) 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 X and
A4: for x being object st x in the carrier of X holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
defpred S₂[ Element of X, Nat, set ] means ex g0 being sequence of the carrier of X st
( g0 = f . $1 & $3 = g0 . $2 );
A5: for a being Element of X
for n being Nat ex b being Element of X st S₂[a,n,b]

proof

let a be Element of X; :: thesis: for n being Nat ex b being Element of X st S₂[a,n,b]
let n be Nat; :: thesis: ex b being Element of X st S₂[a,n,b]
consider g0 being sequence of the carrier of X, h being Element of X such that
a = h and
A6: g0 = f . a and
g0 . 0 = 0. X 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 X,NAT:], the carrier of X such that
A7: for a being Element of X
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 X holds
( F . (h,0) = 0. X & ( for n being Nat holds F . (h,(n + 1)) = (F . (h,n)) * h ) )
let h be Element of X; :: thesis: ( F . (h,0) = 0. X & ( for n being Nat holds F . (h,(n + 1)) = (F . (h,n)) * h ) )
A8: ex g2 being sequence of the carrier of X ex b being Element of X st
( h = b & g2 = f . h & g2 . 0 = 0. X & ( for n being Nat holds g2 . (n + 1) = (g2 . n) * b ) ) by A4;
ex g1 being sequence of the carrier of X st
( g1 = f . h & F . (h,0) = g1 . 0 ) by A7;
hence F . (h,0) = 0. X 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 X ex b being Element of X st
( h = b & g2 = f . h & g2 . 0 = 0. X & ( for n being Nat holds g2 . (n + 1) = (g2 . n) * b ) ) by A4;
( ex g0 being sequence of the carrier of X st
( g0 = f . h & F . (h,n) = g0 . n ) & ex g1 being sequence of the carrier of X 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