:: deftheorem defines MXF2MXR MATRIXR1:def 2 :
for A being Matrix of F_Real holds MXF2MXR A = A;