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