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