theorem :: MATRIX_6:15

for K being Field
for n being Nat
for M1, M2 being Matrix of n,K st M2 is_reverse_of M1 holds
M1 commutes_with M2 ;