defpred S_{1}[ Nat, set , set ] means ( ( $2 is not PartFunc of X,COMPLEX & $3 = F . $1 ) or ( $2 is PartFunc of X,COMPLEX & ( for F2 being PartFunc of X,COMPLEX st F2 = $2 holds

$3 = F2 + (F . ($1 + 1)) ) ) );

A1: for n being Nat

for x being set ex y being set st S_{1}[n,x,y]

A2: ( dom IT = NAT & IT . 0 = F . 0 & ( for n being Nat holds S_{1}[n,IT . n,IT . (n + 1)] ) )
from RECDEF_1:sch 1(A1);

then reconsider IT = IT as Functional_Sequence of X,COMPLEX by A2, FUNCT_2:def 1, RELSET_1:4;

take IT ; :: thesis: ( IT . 0 = F . 0 & ( for n being Nat holds IT . (n + 1) = (IT . n) + (F . (n + 1)) ) )

thus ( IT . 0 = F . 0 & ( for n being Nat holds IT . (n + 1) = (IT . n) + (F . (n + 1)) ) ) by A2; :: thesis: verum

$3 = F2 + (F . ($1 + 1)) ) ) );

A1: for n being Nat

for x being set ex y being set st S

proof

consider IT being Function such that
let n be Nat; :: thesis: for x being set ex y being set st S_{1}[n,x,y]

let x be set ; :: thesis: ex y being set st S_{1}[n,x,y]

_{1}[n,x,y]
; :: thesis: verum

end;let x be set ; :: thesis: ex y being set st S

now :: thesis: ( x is PartFunc of X,COMPLEX implies ex y being Element of K16(K17(X,COMPLEX)) st

( ( x is not PartFunc of X,COMPLEX & y = F . n ) or ( x is PartFunc of X,COMPLEX & ( for F2 being PartFunc of X,COMPLEX st F2 = x holds

y = F2 + (F . (n + 1)) ) ) ) )

hence
ex y being set st S( ( x is not PartFunc of X,COMPLEX & y = F . n ) or ( x is PartFunc of X,COMPLEX & ( for F2 being PartFunc of X,COMPLEX st F2 = x holds

y = F2 + (F . (n + 1)) ) ) ) )

assume
x is PartFunc of X,COMPLEX
; :: thesis: ex y being Element of K16(K17(X,COMPLEX)) st

( ( x is not PartFunc of X,COMPLEX & y = F . n ) or ( x is PartFunc of X,COMPLEX & ( for F2 being PartFunc of X,COMPLEX st F2 = x holds

y = F2 + (F . (n + 1)) ) ) )

then reconsider G2 = x as PartFunc of X,COMPLEX ;

take y = G2 + (F . (n + 1)); :: thesis: ( ( x is not PartFunc of X,COMPLEX & y = F . n ) or ( x is PartFunc of X,COMPLEX & ( for F2 being PartFunc of X,COMPLEX st F2 = x holds

y = F2 + (F . (n + 1)) ) ) )

thus ( ( x is not PartFunc of X,COMPLEX & y = F . n ) or ( x is PartFunc of X,COMPLEX & ( for F2 being PartFunc of X,COMPLEX st F2 = x holds

y = F2 + (F . (n + 1)) ) ) ) ; :: thesis: verum

end;( ( x is not PartFunc of X,COMPLEX & y = F . n ) or ( x is PartFunc of X,COMPLEX & ( for F2 being PartFunc of X,COMPLEX st F2 = x holds

y = F2 + (F . (n + 1)) ) ) )

then reconsider G2 = x as PartFunc of X,COMPLEX ;

take y = G2 + (F . (n + 1)); :: thesis: ( ( x is not PartFunc of X,COMPLEX & y = F . n ) or ( x is PartFunc of X,COMPLEX & ( for F2 being PartFunc of X,COMPLEX st F2 = x holds

y = F2 + (F . (n + 1)) ) ) )

thus ( ( x is not PartFunc of X,COMPLEX & y = F . n ) or ( x is PartFunc of X,COMPLEX & ( for F2 being PartFunc of X,COMPLEX st F2 = x holds

y = F2 + (F . (n + 1)) ) ) ) ; :: thesis: verum

A2: ( dom IT = NAT & IT . 0 = F . 0 & ( for n being Nat holds S

now :: thesis: for f being object st f in rng IT holds

f in PFuncs (X,COMPLEX)

then
rng IT c= PFuncs (X,COMPLEX)
by TARSKI:def 3;f in PFuncs (X,COMPLEX)

defpred S_{2}[ Nat] means IT . $1 is PartFunc of X,COMPLEX;

let f be object ; :: thesis: ( f in rng IT implies f in PFuncs (X,COMPLEX) )

assume f in rng IT ; :: thesis: f in PFuncs (X,COMPLEX)

then consider m being object such that

A3: m in dom IT and

A4: f = IT . m by FUNCT_1:def 3;

reconsider m = m as Element of NAT by A2, A3;

A5: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]
_{2}[ 0 ]
by A2;

for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A6, A5);

then IT . m is PartFunc of X,COMPLEX ;

hence f in PFuncs (X,COMPLEX) by A4, PARTFUN1:45; :: thesis: verum

end;let f be object ; :: thesis: ( f in rng IT implies f in PFuncs (X,COMPLEX) )

assume f in rng IT ; :: thesis: f in PFuncs (X,COMPLEX)

then consider m being object such that

A3: m in dom IT and

A4: f = IT . m by FUNCT_1:def 3;

reconsider m = m as Element of NAT by A2, A3;

A5: for n being Nat st S

S

proof

A6:
S
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume S_{2}[n]
; :: thesis: S_{2}[n + 1]

then reconsider F2 = IT . n as PartFunc of X,COMPLEX ;

IT . (n + 1) = F2 + (F . (n + 1)) by A2;

hence S_{2}[n + 1]
; :: thesis: verum

end;assume S

then reconsider F2 = IT . n as PartFunc of X,COMPLEX ;

IT . (n + 1) = F2 + (F . (n + 1)) by A2;

hence S

for n being Nat holds S

then IT . m is PartFunc of X,COMPLEX ;

hence f in PFuncs (X,COMPLEX) by A4, PARTFUN1:45; :: thesis: verum

then reconsider IT = IT as Functional_Sequence of X,COMPLEX by A2, FUNCT_2:def 1, RELSET_1:4;

take IT ; :: thesis: ( IT . 0 = F . 0 & ( for n being Nat holds IT . (n + 1) = (IT . n) + (F . (n + 1)) ) )

thus ( IT . 0 = F . 0 & ( for n being Nat holds IT . (n + 1) = (IT . n) + (F . (n + 1)) ) ) by A2; :: thesis: verum