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 5
.= width ((COMPLEX2Field M1) - (COMPLEX2Field M2)) by MATRIX_5:6
.= width ((COMPLEX2Field M1) + (- (COMPLEX2Field M2)))
.= width (COMPLEX2Field M1) by MATRIX_1:def 6
.= 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 5
.= len ((COMPLEX2Field M1) - (COMPLEX2Field M2)) by MATRIX_5:6
.= len ((COMPLEX2Field M1) + (- (COMPLEX2Field M2)))
.= len (COMPLEX2Field M1) by MATRIX_1:def 6
.= len M1 by MATRIX_5:def 1 ;
hence ( len (M1 - M2) = len M1 & width (M1 - M2) = width M1 ) by A1; :: thesis: verum