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