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;

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

( 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;

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