:: deftheorem defines Field2COMPLEX MATRIX_5:def 2 :
for A being Matrix of F_Complex holds Field2COMPLEX A = A;