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 A1: ( nt = idseq (len A) & mt = idseq (width A) ) ; :: thesis: Segm A,nt,mt = A
A2: ( len nt = n & len mt = m & len (idseq (len A)) = len A & len (idseq (width A)) = width A ) by FINSEQ_1:def 18, FINSEQ_1:def 18;

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

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

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

end;

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

then A3: ( len (Segm A,nt,mt) = n & width (Segm A,nt,mt) = m ) by Th1;
then A4: Indices (Segm A,nt,mt) = [:(Seg n),(Seg m):] by MATRIX_1:26;

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 A5: [i,j] in Indices (Segm A,nt,mt) ; :: thesis: (Segm A,nt,mt) * i,j = A * i,j
reconsider i' = i, j' = j as Element of NAT by ORDINAL1:def 13;
( i in Seg n & j in Seg m ) by A4, A5, ZFMISC_1:106;
then ( nt . i' = i & mt . j' = j ) by A1, A2, FINSEQ_2:57;
hence (Segm A,nt,mt) * i,j = A * i,j by A5, Def1; :: thesis: verum

end;

hence Segm A,nt,mt = A by A1, A2, A3, MATRIX_1:21; :: thesis: verum

end;

end;