let D be non empty set ; :: thesis: for A being Matrix of D
for P, P1, Q, Q1, P2, 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, Q, Q1, P2, 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, Q, Q1, P2, 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;
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 A2, A4, Lm2;
set Sq2 = Sgm Q2;
set Sp2 = Sgm P2;
set Sq1 = Sgm Q1;
set Sp1 = Sgm P1;
set S = Segm A,P,Q;
A5: ex q2 being Nat st Q2 c= Seg q2 by Th43;
then A6: rng (Sgm Q2) = Q2 by FINSEQ_1:def 13;
A7: ex p2 being Nat st P2 c= Seg p2 by Th43;
then rng (Sgm P2) = P2 by FINSEQ_1:def 13;
hence A8: [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm A,P1,Q1) by A3, A4, A6, Th55; :: thesis: Segm (Segm A,P1,Q1),P2,Q2 = Segm A,P,Q

now

A9: (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 A10: [i,j] in Indices (Segm A,P,Q) ; :: thesis: (Segm A,P,Q) * i,j = SAA * i,j
A11: [i,j] in Indices SAA by A10, MATRIX_1:27;
then A12: j in Seg (width SAA) by ZFMISC_1:106;
reconsider Sp2i = (Sgm P2) . i, Sq2j = (Sgm Q2) . j as Element of NAT by ORDINAL1:def 13;
A13: (Sgm P1) * (Sgm P2) = Sgm P by A1, A3, Th54;
Indices SAA = [:(Seg (card P2)),(Seg (width SAA)):] by MATRIX_1:26;
then A14: i in Seg (card P2) by A11, ZFMISC_1:106;
then card P2 <> 0 ;
then width SAA = card Q2 by Th1;
then j in dom (Sgm Q2) by A5, A12, FINSEQ_3:45;
then A15: (Sgm Q1) . Sq2j = (Sgm Q) . j by A9, FUNCT_1:23;
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 13;
A16: [i9,j9] in Indices SAA by A10, MATRIX_1:27;
then A17: SAA * i,j = (Segm A,P1,Q1) * Sp2i,Sq2j by Def1;
i in dom (Sgm P2) by A7, A14, FINSEQ_3:45;
then A18: (Sgm P1) . Sp2i = (Sgm P) . i by A13, FUNCT_1:23;
[Sp2i,Sq2j] in Indices (Segm A,P1,Q1) by A8, A16, Th17;
then SAA * i,j = A * ((Sgm P1) . Sp2i),((Sgm Q1) . Sq2j) by A17, Def1;
hence (Segm A,P,Q) * i,j = SAA * i,j by A10, A18, A15, Def1; :: thesis: verum

end;

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