for i, j being Nat
for D being non empty set
for M being Matrix of D st [i,j] in Indices M holds
M * (i,j) = (M . i) . j