let i, j be Element of 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 [i,j] in [:(dom M),(Seg (width M)):] by MATRIX_1:def 5;
then ( i in dom M & j in Seg (width M) ) by ZFMISC_1:106;
hence ( i in Seg (len M) & j in Seg (width M) ) by FINSEQ_1:def 3; :: thesis: verum

end;

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