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