theorem Th11: :: TOPALG_7:11

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 f + g = LoopMlt ((f + c),(c + g))