reconsider g = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
let P be non empty compact Subset of (TOP-REAL 2); ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } implies ex f being Function of (Closed-Interval-TSpace ((- 1),1)),((TOP-REAL 2) | (Upper_Arc P)) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds
f . (q `1) = q ) & f . (- 1) = W-min P & f . 1 = E-max P ) )
set P4 = Lower_Arc P;
set K0 = Upper_Arc P;
reconsider g2 = g | (Upper_Arc P) as Function of ((TOP-REAL 2) | (Upper_Arc P)),R^1 by PRE_TOPC:9;
A1:
for p being Point of ((TOP-REAL 2) | (Upper_Arc P)) holds g2 . p = proj1 . p
assume A2:
P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 }
; ex f being Function of (Closed-Interval-TSpace ((- 1),1)),((TOP-REAL 2) | (Upper_Arc P)) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds
f . (q `1) = q ) & f . (- 1) = W-min P & f . 1 = E-max P )
then reconsider g3 = g2 as continuous Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) by Lm6;
A3:
rng g3 = [#] (Closed-Interval-TSpace ((- 1),1))
by A2, Lm6;
A4:
P is being_simple_closed_curve
by A2, JGRAPH_3:26;
then A5:
(Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)}
by JORDAN6:def 9;
E-max P in {(W-min P),(E-max P)}
by TARSKI:def 2;
then A6:
E-max P in Upper_Arc P
by A5, XBOOLE_0:def 4;
Closed-Interval-TSpace ((- 1),1) = TopSpaceMetr (Closed-Interval-MSpace ((- 1),1))
by TOPMETR:def 7;
then A7:
Closed-Interval-TSpace ((- 1),1) is T_2
by PCOMPS_1:34;
A8:
g3 is one-to-one
by A2, Lm6;
A9:
dom g3 = [#] ((TOP-REAL 2) | (Upper_Arc P))
by FUNCT_2:def 1;
then A10:
dom g3 = Upper_Arc P
by PRE_TOPC:def 5;
A11:
g3 is onto
by A3, FUNCT_2:def 3;
A12:
for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds
(g3 /") . (q `1) = q
W-min P in {(W-min P),(E-max P)}
by TARSKI:def 2;
then A15:
W-min P in Upper_Arc P
by A5, XBOOLE_0:def 4;
A16:
E-max P = |[1,0]|
by A2, Th30;
A17:
W-min P = |[(- 1),0]|
by A2, Th29;
Upper_Arc P is_an_arc_of W-min P, E-max P
by A4, JORDAN6:def 8;
then
( not Upper_Arc P is empty & Upper_Arc P is compact )
by JORDAN5A:1;
then A18:
g3 /" is being_homeomorphism
by A3, A8, A7, COMPTS_1:17, TOPS_2:56;
A19: (g3 /") . 1 =
(g3 /") . (|[1,0]| `1)
by EUCLID:52
.=
E-max P
by A6, A12, A16
;
(g3 /") . (- 1) =
(g3 /") . (|[(- 1),0]| `1)
by EUCLID:52
.=
W-min P
by A15, A12, A17
;
hence
ex f being Function of (Closed-Interval-TSpace ((- 1),1)),((TOP-REAL 2) | (Upper_Arc P)) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds
f . (q `1) = q ) & f . (- 1) = W-min P & f . 1 = E-max P )
by A18, A12, A19; verum