let N be invertible Matrix of 3,F_Real; :: thesis: for N1 being Matrix of 3,F_Real
for M, NR being Matrix of 3,REAL st M = symmetric_3 (1,1,(- 1),0,0,0) & N1 = M & NR = MXF2MXR (N ~) holds
((N @) * N1) * N = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~))
let N1 be Matrix of 3,F_Real; :: thesis: for M, NR being Matrix of 3,REAL st M = symmetric_3 (1,1,(- 1),0,0,0) & N1 = M & NR = MXF2MXR (N ~) holds
((N @) * N1) * N = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~))
let M, NR be Matrix of 3,REAL; :: thesis: ( M = symmetric_3 (1,1,(- 1),0,0,0) & N1 = M & NR = MXF2MXR (N ~) implies ((N @) * N1) * N = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~)) )
assume that
A1: M = symmetric_3 (1,1,(- 1),0,0,0) and
A2: N1 = M and
A3: NR = MXF2MXR (N ~) ; :: thesis: ((N @) * N1) * N = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~))
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 @

proof

A8: MXF2MXR ((MXR2MXF (NR @)) ~) = (MXR2MXF (NR @)) ~ by MATRIXR1:def 2;
MXR2MXF (NR @) = NR @ by MATRIXR1:def 1;
then MXF2MXR ((MXR2MXF (NR @)) ~) = ((N ~) @) ~ by A8, A3, MATRIXR1:def 2
.= ((N @) ~) ~ by MATRIX_6:13 ;
hence MXF2MXR ((MXR2MXF (NR @)) ~) = N @ by MATRIX_6:16; :: thesis: verum

end;

(N @) * N1 = (MXF2MXR ((MXR2MXF (NR @)) ~)) * N2 by A7, ANPROJ_8:17;
hence ((N @) * N1) * N = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~)) by A2, A6, ANPROJ_8:17; :: thesis: verum