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