let D be set ; :: thesis: for i, j being Nat
for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
[i,j] in Indices M
let i, j be Nat; :: thesis: for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds
[i,j] in Indices M
let M be Matrix of D; :: thesis: ( 1 <= i & i <= len M & 1 <= j & j <= width M implies [i,j] in Indices M )
assume ( 1 <= i & i <= len M & 1 <= j & j <= width M ) ; :: thesis: [i,j] in Indices M
then ( i in dom M & j in Seg (width M) ) by FINSEQ_1:1, FINSEQ_3:25;
hence [i,j] in Indices M by ZFMISC_1:87; :: thesis: verum