let i, j be Nat; 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; ( [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 ) )
( 1 <= i & i <= len M & 1 <= j & j <= width M implies [i,j] in Indices M )
assume that
A3:
1 <= i
and
A4:
i <= len M
and
A5:
1 <= j
and
A6:
j <= width M
; [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; verum