theorem :: MATRIX_5:4

for A, B being Matrix of F_Complex st Field2COMPLEX A = Field2COMPLEX B holds
A = B ;