for T being non empty TopStruct
for c being with_endpoints Curve of T
for h being FinSequence of REAL st len h >= 2 & h . 1 = inf (dom c) & h . (len h) = sup (dom c) & h is increasing holds
ex f being FinSequence of Curves T st
( len f = (len h) - 1 & c = Sum f & ( for i being Nat st 1 <= i & i <= len f holds
f /. i = c | [.(h /. i),(h /. (i + 1)).] ) )