theorem Th7: :: MATRIX_6:6

for n being Nat
for R being Ring
for M1 being Matrix of n,R holds M1 commutes_with 1. (R,n)