theorem Th13: :: MATRPROB:13

for i, j being Nat
for D being non empty set
for M being Matrix of D holds
( [i,j] in Indices M iff ( i in dom M & j in dom (M . i) ) )