theorem Th8: :: MATRIX_6:7

for n being Nat
for R being Ring
for M1, M2, M3 being Matrix of n,R st M2 is_reverse_of M3 & M1 is_reverse_of M3 holds
M1 = M2