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 A1: NR = MXF2MXR N ; :: thesis: (MXF2MXR ((MXR2MXF NR) ~)) * NR = 1_Rmatrix 3
A2: N ~ is_reverse_of N by MATRIX_6:def 4;
(MXF2MXR ((MXR2MXF NR) ~)) * NR = (MXF2MXR (N ~)) * (MXF2MXR N) by A1, ANPROJ_8:16
.= MXF2MXR ((N ~) * N) by Lm05
.= 1_Rmatrix 3 by A2, MATRIX_6:def 2 ;
hence (MXF2MXR ((MXR2MXF NR) ~)) * NR = 1_Rmatrix 3 ; :: thesis: verum