theorem :: MATRIX_5:3

for A, B being Matrix of COMPLEX st COMPLEX2Field A = COMPLEX2Field B holds
A = B ;