let n, m, i, j be Nat; :: thesis: 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 )
let D be non empty set ; :: thesis: for M being Matrix of n,m,D st [i,j] in Indices M holds
( 1 <= i & i <= n & 1 <= j & j <= m )
let M be Matrix of n,m,D; :: thesis: ( [i,j] in Indices M implies ( 1 <= i & i <= n & 1 <= j & j <= m ) )
assume Z: [i,j] in Indices M ; :: thesis: ( 1 <= i & i <= n & 1 <= j & j <= m )
A: len M = n by Def3;

per cases ( n = 0 or n > 0 ) by NAT_1:3;

suppose S: n = 0 ; :: thesis: ( 1 <= i & i <= n & 1 <= j & j <= m )

i in dom M by Z, ZFMISC_1:106;
then ( 1 <= i & i <= 0 ) by S, A, FINSEQ_3:27;
hence ( 1 <= i & i <= n & 1 <= j & j <= m ) by XXREAL_0:2; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ( 1 <= i & i <= n & 1 <= j & j <= m )

then m = width M by Th24;
hence ( 1 <= i & i <= n & 1 <= j & j <= m ) by Z, Th1, A; :: thesis: verum

end;

end;