theorem Th30: :: MATRIX_0:30

for D being set
for i, j being Nat
for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
[i,j] in Indices M