theorem Th3: :: PRGCOR_2:3

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