theorem Th24:
for
x0,
y0 being
Point of
(Tunit_circle 2) for
P,
Q being
Path of
x0,
y0 for
F being
Homotopy of
P,
Q for
xt being
Point of
R^1 st
P,
Q are_homotopic &
xt in CircleMap " {x0} holds
ex
yt being
Point of
R^1 ex
Pt,
Qt being
Path of
xt,
yt ex
Ft being
Homotopy of
Pt,
Qt st
(
Pt,
Qt are_homotopic &
F = CircleMap * Ft &
yt in CircleMap " {y0} & ( for
F1 being
Homotopy of
Pt,
Qt st
F = CircleMap * F1 holds
Ft = F1 ) )