:: deftheorem defines - MATRIXR1:def 4 :
for A being Matrix of REAL holds - A = MXF2MXR (- (MXR2MXF A));