:: deftheorem defines 0. MATRIX_3:def 1 :
for K being Ring
for n, m being Nat holds 0. (K,n,m) = n |-> (m |-> (0. K));