for D, E being non empty set
for n, m, i, j being Nat
for M being Matrix of n,m,D st 0 < n & M is Matrix of n,m,E & [i,j] in Indices M holds
M * (i,j) is Element of E