theorem :: PRGCOR_2:4

for a being FinSequence of REAL ex s being XFinSequence of REAL st
( len s = (len a) + 1 & s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) & Sum a = s . (len a) )