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