:: deftheorem defines --> MATRIX_0:def 11 :
for n, m being Nat
for a being object holds (n,m) --> a = n |-> (m |-> a);