let D be non empty set ; :: thesis: for A being Matrix of D
for P, P1, P2, Q, Q1, Q2 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 & P2 = (Sgm P1) " P & Q2 = (Sgm Q1) " Q holds
( [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1)) & Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q) )
let A be Matrix of D; :: thesis: for P, P1, P2, Q, Q1, Q2 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 & P2 = (Sgm P1) " P & Q2 = (Sgm Q1) " Q holds
( [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1)) & Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q) )
let P, P1, P2, Q, Q1, Q2 be finite without_zero Subset of NAT; :: thesis: ( P c= P1 & Q c= Q1 & P2 = (Sgm P1) " P & Q2 = (Sgm Q1) " Q implies ( [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1)) & Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q) ) )
assume that
A1: P c= P1 and
A2: Q c= Q1 and
A3: P2 = (Sgm P1) " P and
A4: Q2 = (Sgm Q1) " Q ; :: thesis: ( [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1)) & Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q) )
set SA = Segm (A,P1,Q1);
A5: card Q = card Q2 by A2, A4, Lm2;
card P = card P2 by A1, A3, Lm2;
then reconsider SAA = Segm ((Segm (A,P1,Q1)),P2,Q2) as Matrix of card P, card Q,D by A5;
set Sq2 = Sgm Q2;
set Sp2 = Sgm P2;
set Sq1 = Sgm Q1;
set Sp1 = Sgm P1;
set S = Segm (A,P,Q);
A7: rng (Sgm Q2) = Q2 by FINSEQ_1:def 14;
rng (Sgm P2) = P2 by FINSEQ_1:def 14;
hence A9: [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1)) by A3, A4, A7, Th55; :: thesis: Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q)

now :: thesis: for i, j being Nat st [i,j] in Indices (Segm (A,P,Q)) holds
(Segm (A,P,Q)) * (i,j) = SAA * (i,j)

A10: (Sgm Q1) * (Sgm Q2) = Sgm Q by A2, A4, Th54;
let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm (A,P,Q)) implies (Segm (A,P,Q)) * (i,j) = SAA * (i,j) )
assume A11: [i,j] in Indices (Segm (A,P,Q)) ; :: thesis: (Segm (A,P,Q)) * (i,j) = SAA * (i,j)
A12: [i,j] in Indices SAA by A11, MATRIX_0:26;
then A13: j in Seg (width SAA) by ZFMISC_1:87;
reconsider Sp2i = (Sgm P2) . i, Sq2j = (Sgm Q2) . j as Element of NAT by ORDINAL1:def 12;
A14: (Sgm P1) * (Sgm P2) = Sgm P by A1, A3, Th54;
Indices SAA = [:(Seg (card P2)),(Seg (width SAA)):] by MATRIX_0:25;
then A15: i in Seg (card P2) by A12, ZFMISC_1:87;
then card P2 <> 0 ;
then width SAA = card Q2 by Th1;
then j in dom (Sgm Q2) by A13, FINSEQ_3:40;
then A16: (Sgm Q1) . Sq2j = (Sgm Q) . j by A10, FUNCT_1:13;
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;
A17: [i9,j9] in Indices SAA by A11, MATRIX_0:26;
then A18: SAA * (i,j) = (Segm (A,P1,Q1)) * (Sp2i,Sq2j) by Def1;
i in dom (Sgm P2) by A15, FINSEQ_3:40;
then A19: (Sgm P1) . Sp2i = (Sgm P) . i by A14, FUNCT_1:13;
[Sp2i,Sq2j] in Indices (Segm (A,P1,Q1)) by A9, A17, Th17;
then SAA * (i,j) = A * (((Sgm P1) . Sp2i),((Sgm Q1) . Sq2j)) by A18, Def1;
hence (Segm (A,P,Q)) * (i,j) = SAA * (i,j) by A11, A19, A16, Def1; :: thesis: verum

end;

hence Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q) by MATRIX_0:27; :: thesis: verum