let T be non empty TopSpace-like unital BinContinuous TopGrStr ; :: thesis: for t being unital Point of T
for f, g being Loop of t
for c being constant Loop of t holds LoopMlt (f,g), LoopMlt ((f + c),(c + g)) are_homotopic
let t be unital Point of T; :: thesis: for f, g being Loop of t
for c being constant Loop of t holds LoopMlt (f,g), LoopMlt ((f + c),(c + g)) are_homotopic
let f, g be Loop of t; :: thesis: for c being constant Loop of t holds LoopMlt (f,g), LoopMlt ((f + c),(c + g)) are_homotopic
let c be constant Loop of t; :: thesis: LoopMlt (f,g), LoopMlt ((f + c),(c + g)) are_homotopic
( f,f + c are_homotopic & c + g,g are_homotopic ) by BORSUK_6:80, BORSUK_6:82;
hence LoopMlt (f,g), LoopMlt ((f + c),(c + g)) are_homotopic by Th9; :: thesis: verum