for X being non empty set
for F being summable FinSequence of Funcs (X,ExtREAL) st len F >= 2 holds
(Partial_Sums F) /. 2 = (F /. 1) + (F /. 2)