theorem :: MATRIX_6:37

for n being Nat
for K being Field
for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible & M1 commutes_with M2 holds
( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~) * (M2 ~) )