theorem Th9: :: MATRIX_5:9

for K being Field
for M being Matrix of K holds (1_ K) * M = M