for n being Element of NAT
for K being Field
for A being Matrix of n,K holds
( A = 0. (K,n) iff for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
A * (i,j) = 0. K )