defpred S1[ 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 S1[n,x,y]
proof
let n be
Nat;
for x being set ex y being set st S1[n,x,y]let x be
set ;
ex y being set st S1[n,x,y]
thus
ex
y being
set st
S1[
n,
x,
y]
verum
end;
consider IT being Function such that
A3:
( dom IT = NAT & IT . 0 = F . 0 & ( for n being Nat holds S1[n,IT . n,IT . (n + 1)] ) )
from RECDEF_1:sch 1(A1);
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
; ( 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; verum