:: deftheorem DefCSM defines Partial_Sums_in_cod2 DBLSEQ_3:def 14 :
for f, b₂ being Function of [:NAT,NAT:],ExtREAL holds
( b₂ = Partial_Sums_in_cod2 f iff for n, m being Nat holds
( b₂ . (n,0) = f . (n,0) & b₂ . (n,(m + 1)) = (b₂ . (n,m)) + (f . (n,(m + 1))) ) );