let D be non empty set ; :: thesis: for i, j, m, n 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 i, j, m, n 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:124;
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:124;
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:87;
[i,j] in [:(Seg n),(Seg (width (Segm (A,nt,mt)))):] by A4, MATRIX_0:25;
then A6: i in Seg n by ZFMISC_1:87;
then A7: n <> 0 ;
dom nt = Seg n by FINSEQ_2:124;
then A8: nt . i in rng nt by A6, FUNCT_1:def 3;
width (Segm (A,nt,mt)) = m by Th1, A7;
then mt . j in rng mt by A5, A3, FUNCT_1:def 3;
then [(nt . i),(mt . j)] in [:(rng nt),(rng mt):] by A8, ZFMISC_1:87;
hence [(nt . i),(mt . j)] in Indices A by A2; :: thesis: verum
end;
assume A9: [(nt . i),(mt . j)] in Indices A ; :: thesis: [i,j] in Indices (Segm (A,nt,mt))
A10: j in dom mt
proof
assume not j in dom mt ; :: thesis: contradiction
then mt . j = {} by FUNCT_1:def 2;
then 0 in Seg (width A) by A9, ZFMISC_1:87;
hence contradiction by FINSEQ_1:1; :: thesis: verum
end;
A11: i in dom nt
proof
assume not i in dom nt ; :: thesis: contradiction
then A12: nt . i = {} by FUNCT_1:def 2;
dom A = Seg (len A) by FINSEQ_1:def 3;
then 0 in Seg (len A) by A9, A12, ZFMISC_1:87;
hence contradiction by FINSEQ_1:1; :: thesis: verum
end;
then n <> 0 ;
then A13: width (Segm (A,nt,mt)) = m by Th1;
dom nt = Seg n by FINSEQ_2:124;
then [i,j] in [:(Seg n),(Seg (width (Segm (A,nt,mt)))):] by A11, A10, A13, A1, ZFMISC_1:87;
hence [i,j] in Indices (Segm (A,nt,mt)) by MATRIX_0:25; :: thesis: verum