theorem :: MATRIXR1:44
for A being Matrix of REAL st len A > 0 holds
0 * A = 0_Rmatrix ((len A),(width A))