:: deftheorem defines MXR2MXF MATRIXR1:def 1 :
for A being Matrix of REAL holds MXR2MXF A = A;