theorem :: MATRIX_5:6

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