theorem Th7: :: MATRIX_6:7

for n being Nat
for K being Field
for M1, M2, M3 being Matrix of n,K st M2 is_reverse_of M3 & M1 is_reverse_of M3 holds
M1 = M2