theorem Th40: :: ENTROPY1:40

for D being non empty set
for M being Matrix of D
for i, j being Nat st [i,j] in Indices M holds
( ((i - 1) * (width M)) + j in dom (Mx2FinS M) & M * (i,j) = (Mx2FinS M) . (((i - 1) * (width M)) + j) )