let i, j, n, m 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 that
A1: ( 1 <= i & i <= n ) and
A2: ( 1 <= j & j <= m ) ; :: thesis: [i,j] in Indices M
A3: len M = n by Def2;

per cases ( n = 0 or n > 0 ) ;

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

hence [i,j] in Indices M by A1; :: thesis: verum

end;

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

then m = width M by Th23;
hence [i,j] in Indices M by A1, A2, A3, Th30; :: thesis: verum

end;

end;