theorem :: DBLSEQ_2:54

for D being non empty set
for Rseq being Function of [:NAT,NAT:],D
for n, m being Nat ex M being Matrix of n + 1,m + 1,D st
for i, j being Nat st i <= n & j <= m holds
Rseq . (i,j) = M * ((i + 1),(j + 1))