let T be non empty TopSpace; :: thesis: for a, b being Point of T
for P being Path of a,b
for Q being constant Path of b,b st a,b are_connected holds
P + Q,P are_homotopic
let a, b be Point of T; :: thesis: for P being Path of a,b
for Q being constant Path of b,b st a,b are_connected holds
P + Q,P are_homotopic
let P be Path of a,b; :: thesis: for Q being constant Path of b,b st a,b are_connected holds
P + Q,P are_homotopic
let Q be constant Path of b,b; :: thesis: ( a,b are_connected implies P + Q,P are_homotopic )
assume A1: a,b are_connected ; :: thesis: P + Q,P are_homotopic
RePar (P,1RP) = P + Q by A1, Th50;
hence P + Q,P are_homotopic by A1, Th45, Th47; :: thesis: verum