let i, j be Nat; :: thesis: for M being tabular FinSequence holds
( [i,j] in Indices M iff ( 1 <= i & i <= len M & 1 <= j & j <= width M ) )
let M be tabular FinSequence; :: thesis: ( [i,j] in Indices M iff ( 1 <= i & i <= len M & 1 <= j & j <= width M ) )
thus ( [i,j] in Indices M implies ( 1 <= i & i <= len M & 1 <= j & j <= width M ) ) :: thesis: ( 1 <= i & i <= len M & 1 <= j & j <= width M implies [i,j] in Indices M )

proof

assume [i,j] in Indices M ; :: thesis: ( 1 <= i & i <= len M & 1 <= j & j <= width M )
then [i,j] in [:(Seg (len M)),(Seg (width M)):] by FINSEQ_1:def 3;
then ( i in Seg (len M) & j in Seg (width M) ) by ZFMISC_1:106;
hence ( 1 <= i & i <= len M & 1 <= j & j <= width M ) by FINSEQ_1:3; :: thesis: verum

end;

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:3, FINSEQ_3:27;
hence [i,j] in Indices M by ZFMISC_1:106; :: thesis: verum