theorem :: MATRIX_5:8

for A being Matrix of F_Complex holds
( len A = len (Field2COMPLEX A) & width A = width (Field2COMPLEX A) ) ;