for n, m being Nat
for D being non empty set
for a being Element of D holds m |-> (n |-> a) is Matrix of m,n,D