let M be Matrix of COMPLEX; :: thesis: ( len (- M) = len M & width (- M) = width M )
A1: width (- M) = width (COMPLEX2Field (- M)) by MATRIX_5:7
.= width (COMPLEX2Field (Field2COMPLEX (- (COMPLEX2Field M)))) by MATRIX_5:def 4
.= width (- (COMPLEX2Field M)) by MATRIX_5:6
.= width (COMPLEX2Field M) by MATRIX_3:def 2
.= width M by MATRIX_5:def 1 ;
len (- M) = len (COMPLEX2Field (- M)) by MATRIX_5:7
.= len (COMPLEX2Field (Field2COMPLEX (- (COMPLEX2Field M)))) by MATRIX_5:def 4
.= len (- (COMPLEX2Field M)) by MATRIX_5:6
.= len (COMPLEX2Field M) by MATRIX_3:def 2
.= len M by MATRIX_5:def 1 ;
hence ( len (- M) = len M & width (- M) = width M ) by A1; :: thesis: verum