theorem Th12: :: MATRPROB:12

for i, j being Nat
for M being tabular FinSequence holds
( [i,j] in Indices M iff ( i in Seg (len M) & j in Seg (width M) ) )