theorem :: BORSUK_6:81

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