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

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

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

A4: i in dom M by A1, ZFMISC_1:87;
then A5: 1 <= i by FINSEQ_3:25;
i <= 0 by A2, A3, A4, FINSEQ_3:25;
hence ( 1 <= i & i <= n & 1 <= j & j <= m ) by A5; :: thesis: verum

end;

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

then m = width M by Th23;
hence ( 1 <= i & i <= n & 1 <= j & j <= m ) by A1, A2, Th32; :: thesis: verum

end;

end;