theorem Th15: :: MATRPROB:15

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 (Col (M,j)) & j in dom (Line (M,i)) ) )