defpred S₁[ Element of 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 Element of NAT
for x being set ex y being set st S₁[n,x,y]

proof

let n be Element of 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 Element of NAT holds S₁[n,IT . n,IT . (n + 1)] ) ) from RECDEF_1:sch 1(A1);

now

defpred S₂[ Element of NAT ] means IT . $1 is PartFunc of X,ExtREAL;
let f be set ; :: 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 set 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 Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of 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 Element of NAT holds S₂[n] from NAT_1:sch 1(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) by TARSKI:def 3;
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)) ) )
for n being Nat holds IT . (n + 1) = (IT . n) + (F . (n + 1))

proof

let n be Nat; :: thesis: IT . (n + 1) = (IT . n) + (F . (n + 1))
reconsider m = n as Element of NAT by ORDINAL1:def 12;
IT . (m + 1) = (IT . m) + (F . (m + 1)) by A3;
hence IT . (n + 1) = (IT . n) + (F . (n + 1)) ; :: thesis: verum

end;

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