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 P + (- P),Q 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 P + (- P),Q are_homotopic
let P be Path of a1,b1; :: 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
a1,b1 are_connected by BORSUK_2:def 3;
hence P + (- P),Q are_homotopic by Th92; :: thesis: verum