let M1, M2 be Matrix of COMPLEX; :: thesis: ( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 )
A1: width (M1 + M2) = width (COMPLEX2Field (M1 + M2)) by MATRIX_5:7
.= width (COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field M1) + (COMPLEX2Field M2)))) by MATRIX_5:def 3
.= width ((COMPLEX2Field M1) + (COMPLEX2Field M2)) by MATRIX_5:6
.= width (COMPLEX2Field M1) by MATRIX_3:def 3
.= width M1 by MATRIX_5:def 1 ;
len (M1 + M2) = len (COMPLEX2Field (M1 + M2)) by MATRIX_5:7
.= len (COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field M1) + (COMPLEX2Field M2)))) by MATRIX_5:def 3
.= len ((COMPLEX2Field M1) + (COMPLEX2Field M2)) by MATRIX_5:6
.= len (COMPLEX2Field M1) by MATRIX_3:def 3
.= len M1 by MATRIX_5:def 1 ;
hence ( len (M1 + M2) = len M1 & width (M1 + M2) = width M1 ) by A1; :: thesis: verum