theorem :: MATRIX_5:7

for A being Matrix of COMPLEX holds
( len A = len (COMPLEX2Field A) & width A = width (COMPLEX2Field A) ) ;