theorem Th56: :: MATRIX13:56

for D being non empty set
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) )