theorem :: BORSUK_6:83

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 a1,a1 holds Q + P,P are_homotopic by Th82, BORSUK_2:def 3;