let D be non empty set ; :: thesis: for n, m, i, j being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
( [i,j] in Indices (Segm (A,nt,mt)) iff [(nt . i),(mt . j)] in Indices A )
let n, m, i, j be Nat; :: thesis: for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
( [i,j] in Indices (Segm (A,nt,mt)) iff [(nt . i),(mt . j)] in Indices A )
let A be Matrix of D; :: thesis: for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
( [i,j] in Indices (Segm (A,nt,mt)) iff [(nt . i),(mt . j)] in Indices A )
let nt be Element of n -tuples_on NAT; :: thesis: for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
( [i,j] in Indices (Segm (A,nt,mt)) iff [(nt . i),(mt . j)] in Indices A )
let mt be Element of m -tuples_on NAT; :: thesis: ( [:(rng nt),(rng mt):] c= Indices A implies ( [i,j] in Indices (Segm (A,nt,mt)) iff [(nt . i),(mt . j)] in Indices A ) )
set S = Segm (A,nt,mt);
A1: dom mt = Seg m by FINSEQ_2:144;
assume A2: [:(rng nt),(rng mt):] c= Indices A ; :: thesis: ( [i,j] in Indices (Segm (A,nt,mt)) iff [(nt . i),(mt . j)] in Indices A )
thus ( [i,j] in Indices (Segm (A,nt,mt)) implies [(nt . i),(mt . j)] in Indices A ) :: thesis: ( [(nt . i),(mt . j)] in Indices A implies [i,j] in Indices (Segm (A,nt,mt)) )

proof

A3: dom mt = Seg m by FINSEQ_2:144;
assume A4: [i,j] in Indices (Segm (A,nt,mt)) ; :: thesis: [(nt . i),(mt . j)] in Indices A
then A5: j in Seg (width (Segm (A,nt,mt))) by ZFMISC_1:106;
[i,j] in [:(Seg n),(Seg (width (Segm (A,nt,mt)))):] by A4, MATRIX_1:26;
then A6: i in Seg n by ZFMISC_1:106;
then B6: n <> 0 ;
dom nt = Seg n by FINSEQ_2:144;
then A7: nt . i in rng nt by A6, FUNCT_1:def 5;
width (Segm (A,nt,mt)) = m by Th1, B6;
then mt . j in rng mt by A5, A3, FUNCT_1:def 5;
then [(nt . i),(mt . j)] in [:(rng nt),(rng mt):] by A7, ZFMISC_1:106;
hence [(nt . i),(mt . j)] in Indices A by A2; :: thesis: verum

end;

assume A8: [(nt . i),(mt . j)] in Indices A ; :: thesis: [i,j] in Indices (Segm (A,nt,mt))
A9: j in dom mt

proof

assume not j in dom mt ; :: thesis: contradiction
then mt . j = {} by FUNCT_1:def 4;
then 0 in Seg (width A) by A8, ZFMISC_1:106;
hence contradiction by FINSEQ_1:3; :: thesis: verum

end;

A10: i in dom nt

proof

assume not i in dom nt ; :: thesis: contradiction
then A11: nt . i = {} by FUNCT_1:def 4;
dom A = Seg (len A) by FINSEQ_1:def 3;
then 0 in Seg (len A) by A8, A11, ZFMISC_1:106;
hence contradiction by FINSEQ_1:3; :: thesis: verum

end;

then n <> 0 ;
then A12: width (Segm (A,nt,mt)) = m by Th1;
dom nt = Seg n by FINSEQ_2:144;
then [i,j] in [:(Seg n),(Seg (width (Segm (A,nt,mt)))):] by A10, A9, A12, A1, ZFMISC_1:106;
hence [i,j] in Indices (Segm (A,nt,mt)) by MATRIX_1:26; :: thesis: verum