theorem Th1: :: MATRIXC1:1

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