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

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

suppose n = 0 ; :: thesis: [i,j] in Indices M

hence [i,j] in Indices M by Z, XXREAL_0:2; :: thesis: verum

end;

suppose n > 0 ; :: thesis: [i,j] in Indices M

then m = width M by Th24;
hence [i,j] in Indices M by Z, A, Th10; :: thesis: verum

end;

end;