theorem Th37: :: MATRIX_6:36

for n being Nat
for R being Ring
for M1, M2 being Matrix of n,R st M1 is invertible & M2 is invertible holds
( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) )