set Y = 1TopSp {1};
let x0, y0 be Point of (); :: thesis: 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 ) )

let xt be Point of R^1; :: thesis: 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 ) )

let f be Path of x0,y0; :: thesis: ( xt in CircleMap " {x0} implies 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 ) ) )

deffunc H1( set , Element of the carrier of I[01]) -> Element of the carrier of () = f . \$2;
consider F being Function of [: the carrier of (), the carrier of I[01]:], the carrier of () such that
A1: for y being Element of ()
for i being Element of the carrier of I[01] holds F . (y,i) = H1(y,i) from reconsider j = 1 as Point of () by TARSKI:def 1;
A2: [j,j0] in [: the carrier of (),:] by ;
A3: the carrier of [:(),I[01]:] = [: the carrier of (), the carrier of I[01]:] by BORSUK_1:def 2;
then reconsider F = F as Function of [:(),I[01]:],() ;
set Ft = [:(),():] --> xt;
A4: the carrier of [:(),():] = [: the carrier of (), the carrier of ():] by BORSUK_1:def 2;
then A5: for y being Element of ()
for i being Element of holds ([:(),():] --> xt) . [y,i] = xt by ;
A6: [#] () = the carrier of () ;
for p being Point of [:(),I[01]:]
for V being Subset of () st F . p in V & V is open holds
ex W being Subset of [:(),I[01]:] st
( p in W & W is open & F .: W c= V )
proof
let p be Point of [:(),I[01]:]; :: thesis: for V being Subset of () st F . p in V & V is open holds
ex W being Subset of [:(),I[01]:] st
( p in W & W is open & F .: W c= V )

let V be Subset of (); :: thesis: ( F . p in V & V is open implies ex W being Subset of [:(),I[01]:] st
( p in W & W is open & F .: W c= V ) )

assume A7: ( F . p in V & V is open ) ; :: thesis: ex W being Subset of [:(),I[01]:] st
( p in W & W is open & F .: W c= V )

consider p1 being Point of (), p2 being Point of I[01] such that
A8: p = [p1,p2] by BORSUK_1:10;
F . (p1,p2) = f . p2 by A1;
then consider S being Subset of I[01] such that
A9: p2 in S and
A10: S is open and
A11: f .: S c= V by ;
set W = [:{1},S:];
[:{1},S:] c= [: the carrier of (), the carrier of I[01]:] by ZFMISC_1:95;
then reconsider W = [:{1},S:] as Subset of [:(),I[01]:] by BORSUK_1:def 2;
take W ; :: thesis: ( p in W & W is open & F .: W c= V )
thus p in W by ; :: thesis: ( W is open & F .: W c= V )
thus W is open by ; :: thesis: F .: W c= V
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in F .: W or y in V )
assume y in F .: W ; :: thesis: y in V
then consider x being object such that
A12: x in the carrier of [:(),I[01]:] and
A13: x in W and
A14: y = F . x by FUNCT_2:64;
consider x1 being Point of (), x2 being Point of I[01] such that
A15: x = [x1,x2] by ;
x2 in S by ;
then A16: f . x2 in f .: S by FUNCT_2:35;
y = F . (x1,x2) by
.= f . x2 by A1 ;
hence y in V by ; :: thesis: verum
end;
then A17: F is continuous by JGRAPH_2:10;
assume xt in CircleMap " {x0} ; :: thesis: 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 ) )

then A18: CircleMap . xt in {x0} by FUNCT_2:38;
A19: for x being object st x in dom (CircleMap * ([:(),():] --> xt)) holds
(F | [: the carrier of (),:]) . x = (CircleMap * ([:(),():] --> xt)) . x
proof
let x be object ; :: thesis: ( x in dom (CircleMap * ([:(),():] --> xt)) implies (F | [: the carrier of (),:]) . x = (CircleMap * ([:(),():] --> xt)) . x )
assume A20: x in dom (CircleMap * ([:(),():] --> xt)) ; :: thesis: (F | [: the carrier of (),:]) . x = (CircleMap * ([:(),():] --> xt)) . x
consider x1, x2 being object such that
A21: x1 in the carrier of () and
A22: x2 in and
A23: x = [x1,x2] by ;
A24: x2 = 0 by ;
thus (F | [: the carrier of (),:]) . x = F . (x1,x2) by
.= f . x2 by A1, A21, A24, Lm2
.= x0 by
.= CircleMap . xt by
.= CircleMap . (([:(),():] --> xt) . x) by A5, A21, A22, A23
.= (CircleMap * ([:(),():] --> xt)) . x by ; :: thesis: verum
end;
A25: dom (CircleMap * ([:(),():] --> xt)) = [: the carrier of (),:] by ;
A26: dom F = the carrier of [:(),I[01]:] by FUNCT_2:def 1;
then A27: [: the carrier of (),:] c= dom F by ;
then dom (F | [: the carrier of (),:]) = [: the carrier of (),:] by RELAT_1:62;
then consider G being Function of [:(),I[01]:],R^1 such that
A28: G is continuous and
A29: F = CircleMap * G and
A30: G | [: the carrier of (),:] = [:(),():] --> xt and
A31: for H being Function of [:(),I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of (),:] = [:(),():] --> xt holds
G = H by ;
take ft = Prj2 (j,G); :: thesis: ( 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 ) )

thus ft . 0 = G . (j,j0) by Def3
.= ([:(),():] --> xt) . [j,j0] by
.= xt by ; :: thesis: ( 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 ) )

for i being Point of I[01] holds f . i = () . i
proof
let i be Point of I[01]; :: thesis: f . i = () . i
A32: the carrier of [:(),I[01]:] = [: the carrier of (), the carrier of I[01]:] by BORSUK_1:def 2;
thus () . i = CircleMap . (ft . i) by FUNCT_2:15
.= CircleMap . (G . (j,i)) by Def3
.= () . (j,i) by
.= f . i by ; :: thesis: verum
end;
hence f = CircleMap * ft ; :: thesis: ( 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 ) )

thus ft is continuous by A28; :: thesis: for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
ft = f1

let f1 be Function of I[01],R^1; :: thesis: ( f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt implies ft = f1 )
deffunc H2( set , Element of the carrier of I[01]) -> Element of the carrier of R^1 = f1 . \$2;
consider H being Function of [: the carrier of (), the carrier of I[01]:], the carrier of R^1 such that
A33: for y being Element of ()
for i being Element of the carrier of I[01] holds H . (y,i) = H2(y,i) from reconsider H = H as Function of [:(),I[01]:],R^1 by A3;
assume that
A34: f1 is continuous and
A35: f = CircleMap * f1 and
A36: f1 . 0 = xt ; :: thesis: ft = f1
for p being Point of [:(),I[01]:]
for V being Subset of R^1 st H . p in V & V is open holds
ex W being Subset of [:(),I[01]:] st
( p in W & W is open & H .: W c= V )
proof
let p be Point of [:(),I[01]:]; :: thesis: for V being Subset of R^1 st H . p in V & V is open holds
ex W being Subset of [:(),I[01]:] st
( p in W & W is open & H .: W c= V )

let V be Subset of R^1; :: thesis: ( H . p in V & V is open implies ex W being Subset of [:(),I[01]:] st
( p in W & W is open & H .: W c= V ) )

assume A37: ( H . p in V & V is open ) ; :: thesis: ex W being Subset of [:(),I[01]:] st
( p in W & W is open & H .: W c= V )

consider p1 being Point of (), p2 being Point of I[01] such that
A38: p = [p1,p2] by BORSUK_1:10;
H . p = H . (p1,p2) by A38
.= f1 . p2 by A33 ;
then consider W being Subset of I[01] such that
A39: p2 in W and
A40: W is open and
A41: f1 .: W c= V by ;
take W1 = [:([#] ()),W:]; :: thesis: ( p in W1 & W1 is open & H .: W1 c= V )
thus p in W1 by ; :: thesis: ( W1 is open & H .: W1 c= V )
thus W1 is open by ; :: thesis: H .: W1 c= V
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in H .: W1 or y in V )
assume y in H .: W1 ; :: thesis: y in V
then consider c being Element of [:(),I[01]:] such that
A42: c in W1 and
A43: y = H . c by FUNCT_2:65;
consider c1, c2 being object such that
A44: c1 in [#] () and
A45: c2 in W and
A46: c = [c1,c2] by ;
A47: f1 . c2 in f1 .: W by ;
H . c = H . (c1,c2) by A46
.= f1 . c2 by ;
hence y in V by ; :: thesis: verum
end;
then A48: H is continuous by JGRAPH_2:10;
for x being Point of [:(),I[01]:] holds F . x = () . x
proof
let x be Point of [:(),I[01]:]; :: thesis: F . x = () . x
consider x1 being Point of (), x2 being Point of I[01] such that
A49: x = [x1,x2] by BORSUK_1:10;
thus () . x = CircleMap . (H . (x1,x2)) by
.= CircleMap . (f1 . x2) by A33
.= () . x2 by FUNCT_2:15
.= F . (x1,x2) by
.= F . x by A49 ; :: thesis: verum
end;
then A50: F = CircleMap * H ;
for i being Point of I[01] holds ft . i = f1 . i
proof
let i be Point of I[01]; :: thesis: ft . i = f1 . i
A51: dom H = the carrier of [:(),I[01]:] by FUNCT_2:def 1;
then A52: dom (H | [: the carrier of (),:]) = [: the carrier of (),:] by ;
A53: for x being object st x in dom (H | [: the carrier of (),:]) holds
(H | [: the carrier of (),:]) . x = ([:(),():] --> xt) . x
proof
let x be object ; :: thesis: ( x in dom (H | [: the carrier of (),:]) implies (H | [: the carrier of (),:]) . x = ([:(),():] --> xt) . x )
assume A54: x in dom (H | [: the carrier of (),:]) ; :: thesis: (H | [: the carrier of (),:]) . x = ([:(),():] --> xt) . x
then consider x1, x2 being object such that
A55: x1 in the carrier of () and
A56: x2 in and
A57: x = [x1,x2] by ;
A58: x2 = j0 by ;
thus (H | [: the carrier of (),:]) . x = H . (x1,x2) by
.= f1 . x2 by
.= ([:(),():] --> xt) . x by A5, A36, A55, A56, A57, A58 ; :: thesis: verum
end;
dom ([:(),():] --> xt) = [: the carrier of (),:] by ;
then A59: H | [: the carrier of (),:] = [:(),():] --> xt by ;
thus ft . i = G . (j,i) by Def3
.= H . (j,i) by A31, A50, A48, A59
.= f1 . i by A33 ; :: thesis: verum
end;
hence ft = f1 ; :: thesis: verum