theorem :: MEASURE9:14

for D being non empty set
for Y being with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for s1 being sequence of D st ( for n being Nat holds s1 . n = (joined_seq s) . (((Partial_Sums (Length s)) . n) - 1) ) holds
s1 is subsequence of joined_seq s