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