theorem :: TOPALG_1:20

for T being non empty pathwise_connected TopSpace
for a1, b1, c1 being Point of T
for A1, A2 being Path of a1,b1
for B being Path of b1,c1 st A1,A2 are_homotopic holds
A1,(A2 + B) + (- B) are_homotopic