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