let A be Matrix of F_Real; :: thesis: MXR2MXF (MXF2MXR A) = A
MXR2MXF (MXF2MXR A) = MXF2MXR A by MATRIXR1:def 1;
hence MXR2MXF (MXF2MXR A) = A by MATRIXR1:def 2; :: thesis: verum