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 ;
thus len (a * A) = len (MXF2MXR (ea * (MXR2MXF A))) by Def7
.= len A by MATRIX_3:def 5 ; :: thesis: width (a * A) = width A
thus width (a * A) = width (MXF2MXR (ea * (MXR2MXF A))) by Def7
.= width A by MATRIX_3:def 5 ; :: thesis: verum