:: deftheorem defines COMPLEX2Field MATRIX_5:def 1 :
for A being Matrix of COMPLEX holds COMPLEX2Field A = A;