theorem Th9: :: TOPALG_7:9

for T being non empty TopSpace-like unital BinContinuous TopGrStr
for t being unital Point of T
for f1, f2, g1, g2 being Loop of t st f1,f2 are_homotopic & g1,g2 are_homotopic holds
LoopMlt (f1,g1), LoopMlt (f2,g2) are_homotopic