let X be non empty pathwise_connected TopSpace; :: thesis: 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
let a1, b1 be Point of X; :: thesis: for P being Path of a1,b1
for Q being constant Path of a1,a1 holds Q + P,P are_homotopic
let P be Path of a1,b1; :: thesis: for Q being constant Path of a1,a1 holds Q + P,P are_homotopic
let Q be constant Path of a1,a1; :: thesis: Q + P,P are_homotopic
a1,b1 are_connected by BORSUK_2:def 3;
hence Q + P,P are_homotopic by Th90; :: thesis: verum