theorem Th23: :: TOPALG_5:23

for x0, y0 being Point of (Tunit_circle 2)
for xt being Point of R^1
for f being Path of x0,y0 st xt in CircleMap " {x0} holds
ex ft being Function of I[01],R^1 st
( ft . 0 = xt & f = CircleMap * ft & ft is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
ft = f1 ) )