defpred S₁[ Nat, set , set ] means ( ( $2 is not PartFunc of X,ExtREAL & $3 = F . $1 ) or ( $2 is PartFunc of X,ExtREAL & ( for F2 being PartFunc of X,ExtREAL 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]
thus ex y being set st S₁[n,x,y] :: thesis: verum

proof

per cases ( not x is PartFunc of X,ExtREAL or x is PartFunc of X,ExtREAL ) ;

suppose A2: x is not PartFunc of X,ExtREAL ; :: thesis: ex y being set st S₁[n,x,y]

take y = F . n; :: thesis: S₁[n,x,y]
thus ( ( x is not PartFunc of X,ExtREAL & y = F . n ) or ( x is PartFunc of X,ExtREAL & ( for F2 being PartFunc of X,ExtREAL st F2 = x holds
y = F2 + (F . (n + 1)) ) ) ) by A2; :: thesis: verum

end;

suppose x is PartFunc of X,ExtREAL ; :: thesis: ex y being set st S₁[n,x,y]

then reconsider G2 = x as PartFunc of X,ExtREAL ;
take y = G2 + (F . (n + 1)); :: thesis: S₁[n,x,y]
thus ( ( x is not PartFunc of X,ExtREAL & y = F . n ) or ( x is PartFunc of X,ExtREAL & ( for F2 being PartFunc of X,ExtREAL st F2 = x holds
y = F2 + (F . (n + 1)) ) ) ) ; :: thesis: verum

end;

end;

end;

end;

consider IT being Function such that
A3: ( 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,ExtREAL)

defpred S₂[ Nat] means IT . $1 is PartFunc of X,ExtREAL;
let f be object ; :: thesis: ( f in rng IT implies f in PFuncs (X,ExtREAL) )
assume f in rng IT ; :: thesis: f in PFuncs (X,ExtREAL)
then consider m being object such that
A4: m in dom IT and
A5: f = IT . m by FUNCT_1:def 3;
reconsider m = m as Element of NAT by A3, A4;
A6: 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,ExtREAL ;
IT . (n + 1) = F2 + (F . (n + 1)) by A3;
hence S₂[n + 1] ; :: thesis: verum

end;

A7: S₂[ 0 ] by A3;
for n being Nat holds S₂[n] from NAT_1:sch 2(A7, A6);
then IT . m is PartFunc of X,ExtREAL ;
hence f in PFuncs (X,ExtREAL) by A5, PARTFUN1:45; :: thesis: verum

end;

then rng IT c= PFuncs (X,ExtREAL) ;
then reconsider IT = IT as Functional_Sequence of X,ExtREAL by A3, 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 A3; :: thesis: verum