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