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 A1: [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 A2: i in Seg (len M) by ZFMISC_1:87;
j in Seg (width M) by A1, ZFMISC_1:87;
hence ( 1 <= i & i <= len M & 1 <= j & j <= width M ) by A2, FINSEQ_1:1; :: thesis: verum
end;
assume that
A3: 1 <= i and
A4: i <= len M and
A5: 1 <= j and
A6: j <= width M ; :: thesis: [i,j] in Indices M
A7: j in Seg (width M) by A5, A6, FINSEQ_1:1;
i in dom M by A3, A4, FINSEQ_3:25;
hence [i,j] in Indices M by A7, ZFMISC_1:87; :: thesis: verum