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

hereby :: thesis: ( i in Seg (len M) & j in Seg (width M) implies [i,j] in Indices M )

assume [i,j] in Indices M ; :: thesis: ( i in Seg (len M) & j in Seg (width M) )
then A1: [i,j] in [:(dom M),(Seg (width M)):] by MATRIX_0:def 4;
then i in dom M by ZFMISC_1:87;
hence ( i in Seg (len M) & j in Seg (width M) ) by A1, FINSEQ_1:def 3, ZFMISC_1:87; :: thesis: verum

end;

assume that
A2: i in Seg (len M) and
A3: j in Seg (width M) ; :: thesis: [i,j] in Indices M
i in dom M by A2, FINSEQ_1:def 3;
then [i,j] in [:(dom M),(Seg (width M)):] by A3, ZFMISC_1:87;
hence [i,j] in Indices M by MATRIX_0:def 4; :: thesis: verum