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