theorem :: BKMODEL1:64

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
((((M @) * O) @) * O) * ((M @) * O) = (ra ^2) * O