:: deftheorem defines 0. MATRIX_1:def 2 :
for K being non empty doubleLoopStr
for n being Nat holds 0. (K,n) = n |-> (n |-> (0. K));