let O, N be Matrix of 3,REAL; ((((N @) * O) @) * O) * ((N @) * O) = ((O @) * ((N * O) * (N @))) * O
((((N @) * O) @) * O) * ((N @) * O) =
(((O @) * ((N @) @)) * O) * ((N @) * O)
by MATRIXR2:30
.=
(((O @) * N) * O) * ((N @) * O)
by MATRIXR2:29
.=
((O @) * (N * O)) * ((N @) * O)
by MATRIXR2:27
.=
(O @) * ((N * O) * ((N @) * O))
by MATRIXR2:27
.=
(O @) * (((N * O) * (N @)) * O)
by MATRIXR2:27
;
hence
((((N @) * O) @) * O) * ((N @) * O) = ((O @) * ((N * O) * (N @))) * O
by MATRIXR2:27; verum