theorem :: MATRIX_5:5

for A being Matrix of COMPLEX holds A = Field2COMPLEX (COMPLEX2Field A) ;