for T being non empty TopSpace
for c1, c2, c3, c4, c5, c6 being with_endpoints Curve of T st c1,c2 are_homotopic & dom c1 = dom c2 & c3,c4 are_homotopic & dom c3 = dom c4 & c5 = c1 + c3 & c6 = c2 + c4 & the_last_point_of c1 = the_first_point_of c3 & sup (dom c1) = inf (dom c3) holds
c5,c6 are_homotopic