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 ) )
assume A1: [:(rng nt),(rng mt):] c= Indices A ; :: thesis: ( [i,j] in Indices (Segm A,nt,mt) iff [(nt . i),(mt . j)] in Indices A )
set S = Segm A,nt,mt;
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

assume [i,j] in Indices (Segm A,nt,mt) ; :: thesis: [(nt . i),(mt . j)] in Indices A
then [i,j] in [:(Seg n),(Seg (width (Segm A,nt,mt))):] by MATRIX_1:26;
then A2: ( i in Seg n & j in Seg (width (Segm A,nt,mt)) ) by ZFMISC_1:106;
then ( width (Segm A,nt,mt) = m & dom nt = Seg n & dom mt = Seg m ) by Th1, FINSEQ_1:4, FINSEQ_2:144;
then ( nt . i in rng nt & mt . j in rng mt ) by A2, FUNCT_1:def 5;
then [(nt . i),(mt . j)] in [:(rng nt),(rng mt):] by ZFMISC_1:106;
hence [(nt . i),(mt . j)] in Indices A by A1; :: thesis: verum

end;

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

proof

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

end;

A5: 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 A3, ZFMISC_1:106;
hence contradiction by FINSEQ_1:3; :: thesis: verum

end;

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