let D be non empty set ; :: thesis: for 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 nt = idseq (len A) & mt = idseq (width A) holds
Segm (A,nt,mt) = A
let 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 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 CARD_1:def 7;
A4: len (idseq (width A)) = width A by CARD_1:def 7;
A5: len (idseq (len A)) = len A by CARD_1:def 7;
A6: len mt = m by CARD_1:def 7;

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_0:def 2;
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_0:25;

A12: now :: thesis: for i, j being Nat st [i,j] in Indices (Segm (A,nt,mt)) holds
(Segm (A,nt,mt)) * (i,j) = A * (i,j)

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 12;
j in Seg m by A10, A13, ZFMISC_1:87;
then A14: mt . j9 = j by A2, A6, A4, FINSEQ_2:49;
i in Seg n by A11, A13, ZFMISC_1:87;
then nt . i9 = i by A1, A3, A5, FINSEQ_2:49;
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_0:21; :: thesis: verum

end;

end;