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))) by MATRIX_4:def 1
.= 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 5
.= len ((COMPLEX2Field M1) - (COMPLEX2Field M2)) by MATRIX_5:6
.= len ((COMPLEX2Field M1) + (- (COMPLEX2Field M2))) by MATRIX_4:def 1
.= 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