:: deftheorem Def4 defines joined_seq MEASURE9:def 4 :
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 b₄ being sequence of D holds
( b₄ = joined_seq s iff for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & b₄ . n = (s . k) . m ) );