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); :: thesis: ( 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) | (Lower_Arc P)) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
f . (q `1) = q ) & f . (- 1) = W-min P & f . 1 = E-max P ) )
set P4 = Lower_Arc P;
set K0 = Lower_Arc P;
reconsider g2 = g | (Lower_Arc P) as Function of ((TOP-REAL 2) | (Lower_Arc P)),R^1 by PRE_TOPC:9;
A1: for p being Point of ((TOP-REAL 2) | (Lower_Arc P)) holds g2 . p = proj1 . p

proof

let p be Point of ((TOP-REAL 2) | (Lower_Arc P)); :: thesis: g2 . p = proj1 . p
p in the carrier of ((TOP-REAL 2) | (Lower_Arc P)) ;
then p in Lower_Arc P by PRE_TOPC:8;
hence g2 . p = proj1 . p by FUNCT_1:49; :: thesis: verum

end;

assume A2: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } ; :: thesis: ex f being Function of (Closed-Interval-TSpace ((- 1),1)),((TOP-REAL 2) | (Lower_Arc P)) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Lower_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) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) by Lm5;
A3: rng g3 = [#] (Closed-Interval-TSpace ((- 1),1)) by A2, Lm5;
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 Lower_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, Lm5;
A9: dom g3 = [#] ((TOP-REAL 2) | (Lower_Arc P)) by FUNCT_2:def 1;
then A10: dom g3 = Lower_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 Lower_Arc P holds
(g3 /") . (q `1) = q

proof

reconsider g4 = g3 as Function ;
let q be Point of (TOP-REAL 2); :: thesis: ( q in Lower_Arc P implies (g3 /") . (q `1) = q )
A13: ( q in dom g4 implies ( q = (g4 ") . (g4 . q) & q = ((g4 ") * g4) . q ) ) by A8, FUNCT_1:34;
assume A14: q in Lower_Arc P ; :: thesis: (g3 /") . (q `1) = q
then g3 . q = proj1 . q by A1, A10
.= q `1 by PSCOMP_1:def 5 ;
hence (g3 /") . (q `1) = q by A11, A9, A8, A14, A13, PRE_TOPC:def 5, TOPS_2:def 4; :: thesis: verum

end;

W-min P in {(W-min P),(E-max P)} by TARSKI:def 2;
then A15: W-min P in Lower_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;
Lower_Arc P is_an_arc_of E-max P, W-min P by A4, JORDAN6:def 9;
then ( not Lower_Arc P is empty & Lower_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) | (Lower_Arc P)) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
f . (q `1) = q ) & f . (- 1) = W-min P & f . 1 = E-max P ) by A18, A12, A19; :: thesis: verum