theorem Th10: :: MESFUN12:10

for X being non empty set
for F being summable FinSequence of Funcs (X,ExtREAL) holds
( dom F = dom (Partial_Sums F) & ( for n being Nat st n in dom F holds
(Partial_Sums F) /. n = (Partial_Sums F) . n ) & ( for n being Nat
for x being Element of X st 1 <= n & n < len F holds
((Partial_Sums F) /. (n + 1)) . x = (((Partial_Sums F) /. n) . x) + ((F /. (n + 1)) . x) ) )