for T being non empty TopSpace-like unital BinContinuous TopGrStr
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