let D be non empty set ; 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; 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; 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; 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; ( [:(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
; ( [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 )
( [(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))
;
[(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;
verum
end;
assume A9:
[(nt . i),(mt . j)] in Indices A
; [i,j] in Indices (Segm (A,nt,mt))
A10:
j in dom mt
A11:
i in dom nt
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; verum