theorem :: MATRIX_6:43

for n being Nat
for K being Ring
for M1 being Matrix of n,K st M1 is Orthogonal holds
(M1 @) * M1 = M1 * (M1 @)