set Y = 1TopSp {1};
let x0, y0 be Point of (Tunit_circle 2); :: thesis:
let xt be Point of R^1; :: thesis:
let f be Path of x0,y0; :: thesis:
deffunc H₁( set , Element of the carrier of I[01]) -> Element of the carrier of (Tunit_circle 2) = f . $2;
consider F being Function of [: the carrier of (1TopSp {1}), the carrier of I[01]:], the carrier of (Tunit_circle 2) such that
A1: for y being Element of (1TopSp {1})
for i being Element of the carrier of I[01] holds F . (y,i) = H₁(y,i) from BINOP_1:sch 4();
reconsider j = 1 as Point of (1TopSp {1}) by TARSKI:def 1;
A2: [j,j0] in [: the carrier of (1TopSp {1}),{0}:] by Lm4, ZFMISC_1:87;
A3: the carrier of [:(1TopSp {1}),I[01]:] = [: the carrier of (1TopSp {1}), the carrier of I[01]:] by BORSUK_1:def 2;
then reconsider F = F as Function of [:(1TopSp {1}),I[01]:],(Tunit_circle 2) ;
set Ft = [:(1TopSp {1}),(Sspace 0[01]):] --> xt;
A4: the carrier of [:(1TopSp {1}),(Sspace 0[01]):] = [: the carrier of (1TopSp {1}), the carrier of (Sspace 0[01]):] by BORSUK_1:def 2;
then A5: for y being Element of (1TopSp {1})
for i being Element of {0} holds ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . [y,i] = xt by Lm14, FUNCOP_1:7;
A6: [#] (1TopSp {1}) = the carrier of (1TopSp {1}) ;
for p being Point of [:(1TopSp {1}),I[01]:]
for V being Subset of (Tunit_circle 2) st F . p in V & V is open holds
ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & F .: W c= V )

proof

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

end;

then A17: F is continuous by JGRAPH_2:10;
assume xt in CircleMap " {x0} ; :: thesis:
then A18: CircleMap . xt in {x0} by FUNCT_2:38;
A19: for x being object st x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) holds
(F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x

proof

let x be object ; :: thesis:
assume A20: x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) ; :: thesis:
consider x1, x2 being object such that
A21: x1 in the carrier of (1TopSp {1}) and
A22: x2 in {0} and
A23: x = [x1,x2] by A4, A20, Lm14, ZFMISC_1:def 2;
A24: x2 = 0 by A22, TARSKI:def 1;
thus (F | [: the carrier of (1TopSp {1}),{0}:]) . x = F . (x1,x2) by A4, A20, A23, Lm14, FUNCT_1:49
.= f . x2 by A1, A21, A24, Lm2
.= x0 by A24, BORSUK_2:def 4
.= CircleMap . xt by A18, TARSKI:def 1
.= CircleMap . (([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x) by A5, A21, A22, A23
.= (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x by A20, FUNCT_1:12 ; :: thesis:

end;

A25: dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) = [: the carrier of (1TopSp {1}),{0}:] by A4, Lm14, FUNCT_2:def 1;
A26: dom F = the carrier of [:(1TopSp {1}),I[01]:] by FUNCT_2:def 1;
then A27: [: the carrier of (1TopSp {1}),{0}:] c= dom F by A3, Lm3, ZFMISC_1:95;
then dom (F | [: the carrier of (1TopSp {1}),{0}:]) = [: the carrier of (1TopSp {1}),{0}:] by RELAT_1:62;
then consider G being Function of [:(1TopSp {1}),I[01]:],R^1 such that
A28: G is continuous and
A29: F = CircleMap * G and
A30: G | [: the carrier of (1TopSp {1}),{0}:] = [:(1TopSp {1}),(Sspace 0[01]):] --> xt and
A31: for H being Function of [:(1TopSp {1}),I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of (1TopSp {1}),{0}:] = [:(1TopSp {1}),(Sspace 0[01]):] --> xt holds
G = H by A17, A25, A19, Th22, FUNCT_1:2;
take ft = Prj2 (j,G); :: thesis:
thus ft . 0 = G . (j,j0) by Def3
.= ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . [j,j0] by A30, A2, FUNCT_1:49
.= xt by A5, Lm4 ; :: thesis:
for i being Point of I[01] holds f . i = (CircleMap * ft) . i

proof

let i be Point of I[01]; :: thesis:
A32: the carrier of [:(1TopSp {1}),I[01]:] = [: the carrier of (1TopSp {1}), the carrier of I[01]:] by BORSUK_1:def 2;
thus (CircleMap * ft) . i = CircleMap . (ft . i) by FUNCT_2:15
.= CircleMap . (G . (j,i)) by Def3
.= (CircleMap * G) . (j,i) by A32, BINOP_1:18
.= f . i by A1, A29 ; :: thesis:

end;

hence f = CircleMap * ft ; :: thesis:
thus ft is continuous by A28; :: thesis:
let f1 be Function of I[01],R^1; :: thesis:
deffunc H₂( 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 (1TopSp {1}), the carrier of I[01]:], the carrier of R^1 such that
A33: for y being Element of (1TopSp {1})
for i being Element of the carrier of I[01] holds H . (y,i) = H₂(y,i) from BINOP_1:sch 4();
reconsider H = H as Function of [:(1TopSp {1}),I[01]:],R^1 by A3;
assume that
A34: f1 is continuous and
A35: f = CircleMap * f1 and
A36: f1 . 0 = xt ; :: thesis:
for p being Point of [:(1TopSp {1}),I[01]:]
for V being Subset of R^1 st H . p in V & V is open holds
ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & H .: W c= V )

proof

let p be Point of [:(1TopSp {1}),I[01]:]; :: thesis:
let V be Subset of R^1; :: thesis:
assume A37: ( H . p in V & V is open ) ; :: thesis:
consider p1 being Point of (1TopSp {1}), 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 A34, A37, JGRAPH_2:10;
take W1 = [:([#] (1TopSp {1})),W:]; :: thesis:
thus p in W1 by A38, A39, ZFMISC_1:87; :: thesis:
thus W1 is open by A40, BORSUK_1:6; :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in H .: W1 ; :: thesis:
then consider c being Element of [:(1TopSp {1}),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 [#] (1TopSp {1}) and
A45: c2 in W and
A46: c = [c1,c2] by A42, ZFMISC_1:def 2;
A47: f1 . c2 in f1 .: W by A45, FUNCT_2:35;
H . c = H . (c1,c2) by A46
.= f1 . c2 by A33, A44, A45 ;
hence y in V by A41, A43, A47; :: thesis:

end;

then A48: H is continuous by JGRAPH_2:10;
for x being Point of [:(1TopSp {1}),I[01]:] holds F . x = (CircleMap * H) . x

proof

let x be Point of [:(1TopSp {1}),I[01]:]; :: thesis:
consider x1 being Point of (1TopSp {1}), x2 being Point of I[01] such that
A49: x = [x1,x2] by BORSUK_1:10;
thus (CircleMap * H) . x = CircleMap . (H . (x1,x2)) by A49, FUNCT_2:15
.= CircleMap . (f1 . x2) by A33
.= (CircleMap * f1) . x2 by FUNCT_2:15
.= F . (x1,x2) by A1, A35
.= F . x by A49 ; :: thesis:

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:
A51: dom H = the carrier of [:(1TopSp {1}),I[01]:] by FUNCT_2:def 1;
then A52: dom (H | [: the carrier of (1TopSp {1}),{0}:]) = [: the carrier of (1TopSp {1}),{0}:] by A26, A27, RELAT_1:62;
A53: for x being object st x in dom (H | [: the carrier of (1TopSp {1}),{0}:]) holds
(H | [: the carrier of (1TopSp {1}),{0}:]) . x = ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x

proof

let x be object ; :: thesis:
assume A54: x in dom (H | [: the carrier of (1TopSp {1}),{0}:]) ; :: thesis:
then consider x1, x2 being object such that
A55: x1 in the carrier of (1TopSp {1}) and
A56: x2 in {0} and
A57: x = [x1,x2] by A52, ZFMISC_1:def 2;
A58: x2 = j0 by A56, TARSKI:def 1;
thus (H | [: the carrier of (1TopSp {1}),{0}:]) . x = H . (x1,x2) by A54, A57, FUNCT_1:47
.= f1 . x2 by A33, A55, A58
.= ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x by A5, A36, A55, A56, A57, A58 ; :: thesis:

end;

dom ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) = [: the carrier of (1TopSp {1}),{0}:] by A4, Lm14, FUNCT_2:def 1;
then A59: H | [: the carrier of (1TopSp {1}),{0}:] = [:(1TopSp {1}),(Sspace 0[01]):] --> xt by A26, A27, A51, A53, RELAT_1:62;
thus ft . i = G . (j,i) by Def3
.= H . (j,i) by A31, A50, A48, A59
.= f1 . i by A33 ; :: thesis:

end;

hence ft = f1 ; :: thesis: