let a be Real; :: thesis: for A being Matrix of REAL holds
( len (a * A) = len A & width (a * A) = width A )
let A be Matrix of REAL; :: thesis: ( len (a * A) = len A & width (a * A) = width A )
reconsider ea = a as Element of F_Real by XREAL_0:def 1;
A1: width (a * A) = width (MXR2MXF (MXF2MXR (ea * (MXR2MXF A)))) by MATRIXR1:def 7
.= width A by MATRIX_3:def 5 ;
len (a * A) = len (MXR2MXF (MXF2MXR (ea * (MXR2MXF A)))) by MATRIXR1:def 7
.= len A by MATRIX_3:def 5 ;
hence ( len (a * A) = len A & width (a * A) = width A ) by A1; :: thesis: verum