theorem :: MATRIXR2:66

for n, m being Nat
for a being Real st n > 0 holds
a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m)