theorem :: MATRIX_3:19

for n being Nat
for K being Ring
for A being Matrix of n,K holds A * (1. (K,n)) = A