let T be 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 a1,c1 st A1,A2 are_homotopic holds
A1,(B + (- B)) + A2 are_homotopic
let a1, b1, c1 be Point of T; for A1, A2 being Path of a1,b1
for B being Path of a1,c1 st A1,A2 are_homotopic holds
A1,(B + (- B)) + A2 are_homotopic
( a1,b1 are_connected & a1,c1 are_connected )
by BORSUK_2:def 3;
hence
for A1, A2 being Path of a1,b1
for B being Path of a1,c1 st A1,A2 are_homotopic holds
A1,(B + (- B)) + A2 are_homotopic
by Th25; verum