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)) ) ) );
P1: 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 P11: 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 P11; :: 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
P3: ( 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(P1);

now

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
P41: ( m in dom IT & f = IT . m ) by FUNCT_1:def 5;
reconsider m = m as Element of NAT by P41, P3;
defpred S₂[ Element of NAT ] means IT . $1 is PartFunc of X,ExtREAL ;
P42: S₂[ 0 ] by P3;
P43: 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 P3;
hence S₂[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₂[n] from NAT_1:sch 1(P42, P43);
then IT . m is PartFunc of X,ExtREAL ;
hence f in PFuncs X,ExtREAL by P41, PARTFUN1:119; :: 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 P3, FUNCT_2:def 1, RELSET_1:11;
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 13;
IT . (m + 1) = (IT . m) + (F . (m + 1)) by P3;
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 P3; :: thesis: verum