:: deftheorem defines - MATRIX_5:def 5 :
for A, B being Matrix of COMPLEX holds A - B = Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B));