theorem :: MATRIX_8:51

for n being Nat
for K being Field
for M2, M4 being Matrix of n,K st M4 is Orthogonal holds
((M4 @) * M2) * M4 is_similar_to M2