theorem Th14: :: ANPROJ_8:16
for A being Matrix of F_Real holds MXR2MXF (MXF2MXR A) = A