let A be Matrix of REAL; :: thesis: ( len A > 0 implies 0 * A = 0_Rmatrix ((len A),(width A)) )
assume A1: len A > 0 ; :: thesis: 0 * A = 0_Rmatrix ((len A),(width A))
0 * A = MXF2MXR ((0. F_Real) * (MXR2MXF A)) by Def7
.= 0_Rmatrix ((len A),(width A)) by A1, MATRIX_5:24 ;
hence 0 * A = 0_Rmatrix ((len A),(width A)) ; :: thesis: verum