defpred S_{1}[ 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_{1}[x,y]

dom f = the carrier of X and

A4: for x being object st x in the carrier of X holds

S_{1}[x,f . x]
from CLASSES1:sch 1(A1);

defpred S_{2}[ 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_{2}[a,n,b]

A7: for a being Element of X

for n being Nat holds S_{2}[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

( $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

proof

consider f being Function such that
let x be object ; :: thesis: ( x in the carrier of X implies ex y being object st S_{1}[x,y] )

assume x in the carrier of X ; :: thesis: ex y being object st S_{1}[x,y]

then reconsider b = x as Element of X ;

deffunc H_{1}( 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_{1}(n,g0 . n)
from NAT_1:sch 12();

reconsider y = g0 as set ;

take y ; :: thesis: S_{1}[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;assume x in the carrier of X ; :: thesis: ex y being object st S

then reconsider b = x as Element of X ;

deffunc H

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

reconsider y = g0 as set ;

take y ; :: thesis: S

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

dom f = the carrier of X and

A4: for x being object st x in the carrier of X holds

S

defpred S

( 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

proof

consider F being Function of [: the carrier of X,NAT:], the carrier of X such that
let a be Element of X; :: thesis: for n being Nat ex b being Element of X st S_{2}[a,n,b]

let n be Nat; :: thesis: ex b being Element of X st S_{2}[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_{2}[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;let n be Nat; :: thesis: ex b being Element of X st S

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

take g0 ; :: thesis: ( g0 = f . a & g0 . n = g0 . n )

thus ( g0 = f . a & g0 . n = g0 . n ) by A6; :: thesis: verum

A7: for a being Element of X

for n being Nat holds S

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