defpred S₁[ 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₁[n,x,y]

proof

let n be Nat; :: thesis: for x being set ex y being set st S₁[n,x,y]
let x be set ; :: thesis: ex y being set st S₁[n,x,y]

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)) ) ) ) )

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;

hence ex y being set st S₁[n,x,y] ; :: thesis: verum

end;

consider IT being Function such that
A2: ( dom IT = NAT & IT . 0 = F . 0 & ( for n being Nat holds S₁[n,IT . n,IT . (n + 1)] ) ) from RECDEF_1:sch 1(A1);

now :: thesis: for f being object st f in rng IT holds
f in PFuncs (X,COMPLEX)

defpred S₂[ 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₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume S₂[n] ; :: thesis: S₂[n + 1]
then reconsider F2 = IT . n as PartFunc of X,COMPLEX ;
IT . (n + 1) = F2 + (F . (n + 1)) by A2;
hence S₂[n + 1] ; :: thesis: verum

end;

A6: S₂[ 0 ] by A2;
for n being Nat holds S₂[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;

then rng IT c= PFuncs (X,COMPLEX) by TARSKI:def 3;
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