theorem :: MATRIX_8:19

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