:: deftheorem DefCS defines Partial_Sums_in_cod2 DBLSEQ_2:def 2 :
for Rseq, b₂ being Function of [:NAT,NAT:],REAL holds
( b₂ = Partial_Sums_in_cod2 Rseq iff for n, m being Nat holds
( b₂ . (n,0) = Rseq . (n,0) & b₂ . (n,(m + 1)) = (b₂ . (n,m)) + (Rseq . (n,(m + 1))) ) );