:: deftheorem Def2 defines joined_FinSeq MEASURE9:def 2 :
for D being non empty set
for Y being FinSequenceSet of D
for F being FinSequence of Y
for b₄ being FinSequence of D holds
( b₄ = joined_FinSeq F iff ( len b₄ = Sum (Length F) & ( for n being Nat st n in dom b₄ holds
ex k, m being Nat st
( 1 <= m & m <= len (F . (k + 1)) & k < len F & m + (Sum (Length (F | k))) = n & n <= Sum (Length (F | (k + 1))) & b₄ . n = (F . (k + 1)) . m ) ) ) );