theorem Th57: :: MATRIX_6:56
for n being Nat
for R being Ring
for M1, M2, M3 being Matrix of n,R st M1 is invertible & M2 is invertible & M3 is invertible holds
( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~) * (M2 ~)) * (M1 ~) )