theorem
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 for
F being
Homotopy of
f1,
f2 for
G being
Homotopy of
g1,
g2 st
f1,
f2 are_homotopic &
g1,
g2 are_homotopic holds
HomotopyMlt (
F,
G) is
Homotopy of
LoopMlt (
f1,
g1),
LoopMlt (
f2,
g2)