theorem :: BORSUK_6:85

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 P + (- P),Q are_homotopic by Th84, BORSUK_2:def 3;