let D be non empty set ; :: thesis: for n, m 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 nt = idseq (len A) & mt = idseq (width A) holds
Segm A,nt,mt = A
let n, m 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 nt = idseq (len A) & mt = idseq (width A) holds
Segm A,nt,mt = 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 nt = idseq (len A) & mt = idseq (width A) holds
Segm A,nt,mt = A
let nt be Element of n -tuples_on NAT ; :: thesis: for mt being Element of m -tuples_on NAT st nt = idseq (len A) & mt = idseq (width A) holds
Segm A,nt,mt = A
let mt be Element of m -tuples_on NAT ; :: thesis: ( nt = idseq (len A) & mt = idseq (width A) implies Segm A,nt,mt = A )
set S = Segm A,nt,mt;
assume that
A1: nt = idseq (len A) and
A2: mt = idseq (width A) ; :: thesis: Segm A,nt,mt = A
A3: len nt = n by FINSEQ_1:def 18;
A4: len (idseq (width A)) = width A by FINSEQ_1:def 18;
A5: len (idseq (len A)) = len A by FINSEQ_1:def 18;
A6: len mt = m by FINSEQ_1:def 18;

per cases ( n = 0 or n > 0 ) ;

suppose A7: n = 0 ; :: thesis: Segm A,nt,mt = A

then A8: len (Segm A,nt,mt) = 0 by MATRIX_1:def 3;
A = {} by A1, A7;
hence Segm A,nt,mt = A by A8; :: thesis: verum

end;

suppose A9: n > 0 ; :: thesis: Segm A,nt,mt = A

then A10: width (Segm A,nt,mt) = m by Th1;
then A11: Indices (Segm A,nt,mt) = [:(Seg n),(Seg m):] by MATRIX_1:26;

A12: now

let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm A,nt,mt) implies (Segm A,nt,mt) * i,j = A * i,j )
assume A13: [i,j] in Indices (Segm A,nt,mt) ; :: thesis: (Segm A,nt,mt) * i,j = A * i,j
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 13;
j in Seg m by A10, A13, ZFMISC_1:106;
then A14: mt . j9 = j by A2, A6, A4, FINSEQ_2:57;
i in Seg n by A11, A13, ZFMISC_1:106;
then nt . i9 = i by A1, A3, A5, FINSEQ_2:57;
hence (Segm A,nt,mt) * i,j = A * i,j by A13, A14, Def1; :: thesis: verum

end;

len (Segm A,nt,mt) = n by A9, Th1;
hence Segm A,nt,mt = A by A1, A2, A3, A6, A5, A4, A10, A12, MATRIX_1:21; :: thesis: verum

end;

end;