theorem Th41: :: MATRIX_6:40

for n being Nat
for K being Ring
for M1, M2 being Matrix of n,K st M1 is invertible & M1 commutes_with M2 holds
M1 ~ commutes_with M2