theorem Th55: :: BKMODEL1:63

for ra being Real
for O, M being Matrix of 3,REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & M = ra * O holds
( O * M = ra * (1_Rmatrix 3) & M * O = ra * (1_Rmatrix 3) )