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