let N be invertible Matrix of 3,F_Real; :: thesis:
let N1 be Matrix of 3,F_Real; :: thesis:
let M, NR be Matrix of 3,REAL; :: thesis:
assume that
A1: M = symmetric_3 (1,1,(- 1),0,0,0) and
A2: N1 = M and
A3: NR = MXF2MXR (N ~) ; :: thesis:
reconsider b = - 1 as Element of F_Real by XREAL_0:def 1;
A4: not b is zero ;
reconsider a = 1 as Element of F_Real ;
not a is zero ;
then reconsider a = 1, b = - 1 as non zero Element of F_Real by A4;
reconsider N1 = N1 as invertible Matrix of 3,F_Real by A1, A2, Th44;
reconsider M1 = ((N @) * N1) * N as invertible Matrix of 3,F_Real ;
reconsider N2 = N1 as Matrix of 3,REAL ;
A6: MXF2MXR ((MXR2MXF NR) ~) = (MXR2MXF NR) ~ by MATRIXR1:def 2
.= (N ~) ~ by A3, ANPROJ_8:16
.= N by MATRIX_6:16 ;
A7: MXF2MXR ((MXR2MXF (NR @)) ~) = N @

end;