defpred S1[ 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 S1[x,y]
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
S1[x,f . x]
from CLASSES1:sch 1(A1);
defpred S2[ 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 S2[a,n,b]
proof
let a be
Element of
X;
for n being Nat ex b being Element of X st S2[a,n,b]let n be
Nat;
ex b being Element of X st S2[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
;
S2[a,n,g0 . n]
take
g0
;
( g0 = f . a & g0 . n = g0 . n )
thus
(
g0 = f . a &
g0 . n = g0 . n )
by A6;
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 S2[a,n,F . (a,n)]
from NAT_1:sch 19(A5);
take
F
; 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; ( 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; for n being Nat holds F . (h,(n + 1)) = (F . (h,n)) * h
let n be Nat; 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; verum