for T being non empty TopSpace
for c1, c2 being with_endpoints Curve of T
for S being Subset of R^1 st dom c1 = dom c2 & S = dom c1 holds
( c1,c2 are_homotopic iff ex f being Function of [:(R^1 | S),I[01]:],T ex a, b being Point of T st
( f is continuous & ( for t being Point of (R^1 | S) holds
( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) ) )