:: deftheorem defines 0* MATRIX14:def 1 :
for K being non empty ZeroStr
for n being Element of NAT holds 0* (K,n) = n |-> (0. K);