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

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