theorem Th1: :: MATRIX_3:1

for n, m being Nat
for K being Ring
for i, j being Nat st [i,j] in Indices (0. (K,n,m)) holds
(0. (K,n,m)) * (i,j) = 0. K