theorem Th32: :: MATRIX_0:32

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