for F being V251() FinSequence of ExtREAL
for G being ExtREAL_sequence st ( for i being Nat holds F . i = G . i ) holds
for i being Nat holds Sum (F | i) = (Partial_Sums G) . i