let a be Complex; :: thesis: for M being Matrix of COMPLEX holds
( len (a * M) = len M & width (a * M) = width M )
let M be Matrix of COMPLEX; :: thesis: ( len (a * M) = len M & width (a * M) = width M )
a in COMPLEX by XCMPLX_0:def 2;
then reconsider ea = a as Element of F_Complex by COMPLFLD:def 1;
A1: width (a * M) = width (COMPLEX2Field (a * M)) by MATRIX_5:7
.= width (COMPLEX2Field (Field2COMPLEX (ea * (COMPLEX2Field M)))) by MATRIX_5:def 7
.= width (ea * (COMPLEX2Field M)) by MATRIX_5:6
.= width (COMPLEX2Field M) by MATRIX_3:def 5
.= width M by MATRIX_5:def 1 ;
len (a * M) = len (COMPLEX2Field (a * M)) by MATRIX_5:7
.= len (COMPLEX2Field (Field2COMPLEX (ea * (COMPLEX2Field M)))) by MATRIX_5:def 7
.= len (ea * (COMPLEX2Field M)) by MATRIX_5:6
.= len (COMPLEX2Field M) by MATRIX_3:def 5
.= len M by MATRIX_5:def 1 ;
hence ( len (a * M) = len M & width (a * M) = width M ) by A1; :: thesis: verum