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