theorem Th39: :: MATRIX11:39

for n, m being Nat
for D being non empty set
for M being Matrix of n,m,D holds M * (idseq n) = M