theorem :: BKMODEL1:65

for O, N being Matrix of 3,REAL holds ((((N @) * O) @) * O) * ((N @) * O) = ((O @) * ((N * O) * (N @))) * O