for T being non empty TopSpace
for f being FinSequence of Curves T st len f > 0 & ( for i being Nat st 1 <= i & i < len f holds
( (f /. i) . (sup (dom (f /. i))) = (f /. (i + 1)) . (inf (dom (f /. (i + 1)))) & sup (dom (f /. i)) = inf (dom (f /. (i + 1))) ) ) & ( for i being Nat st 1 <= i & i <= len f holds
f /. i is with_endpoints ) holds
ex c being with_endpoints Curve of T st
( Sum f = c & dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) )