theorem :: BORSUK_6:87

for X being non empty pathwise_connected TopSpace
for a1, b1 being Point of X
for P being Path of b1,a1
for Q being constant Path of a1,a1 holds (- P) + P,Q are_homotopic by Th86, BORSUK_2:def 3;