let N be invertible Matrix of 3,F_Real; :: thesis: for NR being Matrix of 3,REAL st NR = MXF2MXR N holds
(MXF2MXR ((MXR2MXF (NR @)) ~)) * (NR @) = 1_Rmatrix 3
let NR be Matrix of 3,REAL; :: thesis: ( NR = MXF2MXR N implies (MXF2MXR ((MXR2MXF (NR @)) ~)) * (NR @) = 1_Rmatrix 3 )
assume NR = MXF2MXR N ; :: thesis: (MXF2MXR ((MXR2MXF (NR @)) ~)) * (NR @) = 1_Rmatrix 3
then NR @ = N @ by MATRIXR1:def 2;
then NR @ = MXF2MXR (N @) by MATRIXR1:def 2;
hence (MXF2MXR ((MXR2MXF (NR @)) ~)) * (NR @) = 1_Rmatrix 3 by Lm10; :: thesis: verum