set Y = 1TopSp {1};

let x0, y0 be Point of (Tunit_circle 2); :: 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 H_{1}( 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_{1}(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 )

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 * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) holds

(F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x

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: ( 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

.= ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . [j,j0] by A30, A2, FUNCT_1:49

.= xt by A5, Lm4 ; :: 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 = (CircleMap * ft) . i

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 H_{2}( 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_{2}(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: ft = f1

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 )

for x being Point of [:(1TopSp {1}),I[01]:] holds F . x = (CircleMap * H) . x

for i being Point of I[01] holds ft . i = f1 . i

let x0, y0 be Point of (Tunit_circle 2); :: 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 H

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

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

then A17:
F is continuous
by JGRAPH_2:10;
let p be Point of [:(1TopSp {1}),I[01]:]; :: thesis: 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 )

let V be Subset of (Tunit_circle 2); :: thesis: ( F . p in V & V is open implies ex W being Subset of [:(1TopSp {1}),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 [:(1TopSp {1}),I[01]:] st

( p in W & W is open & F .: W c= V )

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: ( p in W & W is open & F .: W c= V )

thus p in W by A8, A9, ZFMISC_1:87; :: thesis: ( W is open & F .: W c= V )

thus W is open by A6, A10, BORSUK_1:6; :: 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 [:(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: verum

end;ex W being Subset of [:(1TopSp {1}),I[01]:] st

( p in W & W is open & F .: W c= V )

let V be Subset of (Tunit_circle 2); :: thesis: ( F . p in V & V is open implies ex W being Subset of [:(1TopSp {1}),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 [:(1TopSp {1}),I[01]:] st

( p in W & W is open & F .: W c= V )

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: ( p in W & W is open & F .: W c= V )

thus p in W by A8, A9, ZFMISC_1:87; :: thesis: ( W is open & F .: W c= V )

thus W is open by A6, A10, BORSUK_1:6; :: 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 [:(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: verum

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 * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) holds

(F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x

proof

A25:
dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) = [: the carrier of (1TopSp {1}),{0}:]
by A4, Lm14, FUNCT_2:def 1;
let x be object ; :: thesis: ( x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) implies (F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x )

assume A20: x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) ; :: thesis: (F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x

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: verum

end;assume A20: x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) ; :: thesis: (F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x

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: verum

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: ( 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

.= ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . [j,j0] by A30, A2, FUNCT_1:49

.= xt by A5, Lm4 ; :: 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 = (CircleMap * ft) . i

proof

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
let i be Point of I[01]; :: thesis: f . i = (CircleMap * ft) . i

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: verum

end;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: verum

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 H

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

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: ft = f1

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

then A48:
H is continuous
by JGRAPH_2:10;
let p be Point of [:(1TopSp {1}),I[01]:]; :: thesis: 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 )

let V be Subset of R^1; :: thesis: ( H . p in V & V is open implies ex W being Subset of [:(1TopSp {1}),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 [:(1TopSp {1}),I[01]:] st

( p in W & W is open & H .: W c= V )

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: ( p in W1 & W1 is open & H .: W1 c= V )

thus p in W1 by A38, A39, ZFMISC_1:87; :: thesis: ( W1 is open & H .: W1 c= V )

thus W1 is open by A40, BORSUK_1:6; :: 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 [:(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: verum

end;ex W being Subset of [:(1TopSp {1}),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 [:(1TopSp {1}),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 [:(1TopSp {1}),I[01]:] st

( p in W & W is open & H .: W c= V )

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: ( p in W1 & W1 is open & H .: W1 c= V )

thus p in W1 by A38, A39, ZFMISC_1:87; :: thesis: ( W1 is open & H .: W1 c= V )

thus W1 is open by A40, BORSUK_1:6; :: 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 [:(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: verum

for x being Point of [:(1TopSp {1}),I[01]:] holds F . x = (CircleMap * H) . x

proof

then A50:
F = CircleMap * H
;
let x be Point of [:(1TopSp {1}),I[01]:]; :: thesis: F . x = (CircleMap * H) . x

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: verum

end;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: verum

for i being Point of I[01] holds ft . i = f1 . i

proof

hence
ft = f1
; :: thesis: verum
let i be Point of I[01]; :: thesis: ft . i = f1 . i

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

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: verum

end;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

dom ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) = [: the carrier of (1TopSp {1}),{0}:]
by A4, Lm14, FUNCT_2:def 1;
let x be object ; :: thesis: ( x in dom (H | [: the carrier of (1TopSp {1}),{0}:]) implies (H | [: the carrier of (1TopSp {1}),{0}:]) . x = ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x )

assume A54: x in dom (H | [: the carrier of (1TopSp {1}),{0}:]) ; :: thesis: (H | [: the carrier of (1TopSp {1}),{0}:]) . x = ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x

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: verum

end;assume A54: x in dom (H | [: the carrier of (1TopSp {1}),{0}:]) ; :: thesis: (H | [: the carrier of (1TopSp {1}),{0}:]) . x = ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x

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: verum

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: verum