for n, m being Nat
for Rseq being Function of [:NAT,NAT:],REAL
for M being Matrix of n + 1,m + 1,REAL st ( for i, j being Nat st i <= n & j <= m holds
Rseq . (i,j) = M * ((i + 1),(j + 1)) ) holds
(Partial_Sums Rseq) . (n,m) = SumAll M