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:40 ;
hence 0 * A = 0_Rmatrix (len A),(width A) ; :: thesis: verum