theorem :: BKMODEL1:53

for N being invertible Matrix of 3,F_Real
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) ~))