theorem :: MATRIX_0:33

for i, j, n, m being Nat
for D being non empty set
for M being Matrix of n,m,D st [i,j] in Indices M holds
( 1 <= i & i <= n & 1 <= j & j <= m )