let p1, p2 be Point of (); :: thesis: for P, P1, P2 being non empty Subset of () st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} holds
P is being_simple_closed_curve

reconsider RS = R^2-unit_square as non empty Subset of () ;
let P, P1, P2 be non empty Subset of (); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} implies P is being_simple_closed_curve )
assume that
A1: P1 is_an_arc_of p1,p2 and
A2: P2 is_an_arc_of p1,p2 and
A3: P = P1 \/ P2 and
A4: P1 /\ P2 = {p1,p2} ; :: thesis:
reconsider P9 = P, P19 = P1, P29 = P2 as non empty Subset of () ;
A5: [#] (() | P1) = P1 by PRE_TOPC:def 5;
consider h1, h2 being FinSequence of () such that
A6: h1 is being_S-Seq and
A7: h2 is being_S-Seq and
A8: R^2-unit_square = (L~ h1) \/ (L~ h2) and
A9: (L~ h1) /\ (L~ h2) = {,|[1,1]|} and
A10: h1 /. 1 = and
A11: h1 /. (len h1) = |[1,1]| and
A12: h2 /. 1 = and
A13: h2 /. (len h2) = |[1,1]| by TOPREAL1:24;
A14: len h2 >= 2 by ;
len h1 >= 2 by ;
then reconsider Lh1 = L~ h1, Lh2 = L~ h2 as non empty Subset of () by ;
set T1 = () | Lh1;
set T2 = () | Lh2;
set T = () | RS;
A15: [#] (() | RS) = R^2-unit_square by PRE_TOPC:def 5;
A16: [#] (() | Lh2) = L~ h2 by PRE_TOPC:def 5;
then A17: (TOP-REAL 2) | Lh2 is SubSpace of () | RS by ;
A18: [#] (() | Lh1) = L~ h1 by PRE_TOPC:def 5;
then A19: (TOP-REAL 2) | Lh1 is SubSpace of () | RS by ;
A20: [#] (() | P) = P by PRE_TOPC:def 5;
A21: [#] (() | P2) = P2 by PRE_TOPC:def 5;
then A22: (TOP-REAL 2) | P29 is SubSpace of () | P9 by ;
consider f2 being Function of I,(() | P2) such that
A23: f2 is being_homeomorphism and
A24: f2 . 0 = p1 and
A25: f2 . 1 = p2 by ;
A26: dom f2 = the carrier of I by FUNCT_2:def 1;
P2 c= P by ;
then rng f2 c= the carrier of (() | P) by ;
then reconsider ff2 = f2 as Function of I,(() | P9) by ;
A27: dom ff2 = the carrier of I by FUNCT_2:def 1;
then A28: 0 in dom ff2 by ;
f2 is continuous by A23;
then A29: ff2 is continuous by ;
A30: 1 in dom ff2 by ;
A31: [#] (() | P) = P by PRE_TOPC:def 5;
then A32: (TOP-REAL 2) | P19 is SubSpace of () | P9 by ;
consider f1 being Function of I,(() | P1) such that
A33: f1 is being_homeomorphism and
A34: f1 . 0 = p1 and
A35: f1 . 1 = p2 by ;
A36: dom f1 = the carrier of I by FUNCT_2:def 1;
P1 c= P by ;
then rng f1 c= the carrier of (() | P) by ;
then reconsider ff1 = f1 as Function of I,(() | P9) by ;
A37: dom f1 = the carrier of I by FUNCT_2:def 1;
A38: I is compact by ;
f1 is continuous by A33;
then A39: ff1 is continuous by ;
A40: f1 is one-to-one by A33;
reconsider L1 = L~ h1, L2 = L~ h2 as non empty Subset of () by A9;
L1 is_an_arc_of ,|[1,1]| by ;
then consider g1 being Function of I,(() | L1) such that
A41: g1 is being_homeomorphism and
A42: g1 . 0 = and
A43: g1 . 1 = |[1,1]| by TOPREAL1:def 1;
L2 is_an_arc_of ,|[1,1]| by ;
then consider g2 being Function of I,(() | L2) such that
A44: g2 is being_homeomorphism and
A45: g2 . 0 = and
A46: g2 . 1 = |[1,1]| by TOPREAL1:def 1;
R^2-unit_square = [#] (() | RS) by PRE_TOPC:def 5
.= the carrier of (() | RS) ;
then reconsider p00 = , p11 = |[1,1]| as Point of (() | RS) by ;
A47: (TOP-REAL 2) | RS is T_2 by TOPMETR:2;
set k1 = ff1 * (g1 ");
set k2 = ff2 * (g2 ");
reconsider g1 = g1 as Function of I,(() | Lh1) ;
A48: g1 is one-to-one by A41;
A49: dom g1 = the carrier of I by FUNCT_2:def 1;
A50: rng g1 = [#] (() | Lh1) by A41;
then g1 is onto by FUNCT_2:def 3;
then A51: g1 " = g1 " by ;
then rng (g1 ") = dom g1 by ;
then A52: rng (ff1 * (g1 ")) = rng f1 by
.= P1 by ;
A53: dom g1 = the carrier of I by FUNCT_2:def 1;
then A54: 0 in dom g1 by ;
then A55: 0 = (g1 ") . p00 by ;
A56: dom (g1 ") = rng g1 by ;
then A57: p00 in dom (g1 ") by ;
A58: 1 in dom g1 by ;
then A59: p11 in dom (g1 ") by ;
reconsider g2 = g2 as Function of I,(() | Lh2) ;
A60: g2 is one-to-one by A44;
A61: rng g2 = [#] (() | Lh2) by A44;
then g2 is onto by FUNCT_2:def 3;
then A62: g2 " = g2 " by ;
g2 is continuous by A44;
then A63: (TOP-REAL 2) | Lh2 is compact by ;
A64: g2 " is continuous by A44;
g1 is continuous by A41;
then A65: (TOP-REAL 2) | Lh1 is compact by ;
A66: f2 is one-to-one by A23;
A67: dom g2 = the carrier of I by FUNCT_2:def 1;
then A68: 0 in dom g2 by ;
then A69: p00 in rng g2 by ;
then A70: p00 in dom (g2 ") by ;
(g2 ") . p00 in dom ff2 by ;
then A71: p00 in dom (ff2 * (g2 ")) by ;
A72: dom ff1 = the carrier of I by FUNCT_2:def 1;
then (g1 ") . p00 in dom ff1 by ;
then p00 in dom (ff1 * (g1 ")) by ;
then A73: (ff1 * (g1 ")) . p00 = ff1 . ((g1 ") . p00) by FUNCT_1:12
.= p1 by ;
then A74: (ff1 * (g1 ")) . p00 = ff2 . ((g2 ") . p00) by
.= (ff2 * (g2 ")) . p00 by ;
A75: 1 in dom g2 by ;
then A76: 1 = (g2 ") . p11 by ;
A77: dom (g2 ") = rng g2 by ;
then A78: p11 in dom (g2 ") by ;
(g2 ") . p11 in dom ff2 by ;
then A79: p11 in dom (ff2 * (g2 ")) by ;
(g1 ") . p11 in dom ff1 by ;
then p11 in dom (ff1 * (g1 ")) by ;
then A80: (ff1 * (g1 ")) . p11 = ff1 . ((g1 ") . p11) by FUNCT_1:12
.= p2 by ;
then A81: (ff1 * (g1 ")) . p11 = ff2 . ((g2 ") . p11) by
.= (ff2 * (g2 ")) . p11 by ;
g1 " is continuous by A41;
then reconsider h = (ff1 * (g1 ")) +* (ff2 * (g2 ")) as continuous Function of (() | RS),(() | P) by A8, A9, A39, A29, A18, A16, A15, A65, A63, A47, A64, A74, A81, A19, A17, COMPTS_1:21;
A82: 1 = (g1 ") . p11 by ;
A83: rng (g2 ") = dom g2 by ;
then A84: rng (ff2 * (g2 ")) = rng f2 by
.= [#] (() | P2) by A23
.= P2 by PRE_TOPC:def 5 ;
A85: 0 = (g2 ") . p00 by ;
now :: thesis: for x1, x2 being set st x1 in dom (ff2 * (g2 ")) & x2 in (dom (ff1 * (g1 "))) \ (dom (ff2 * (g2 "))) holds
not (ff2 * (g2 ")) . x1 = (ff1 * (g1 ")) . x2
let x1, x2 be set ; :: thesis: ( x1 in dom (ff2 * (g2 ")) & x2 in (dom (ff1 * (g1 "))) \ (dom (ff2 * (g2 "))) implies not (ff2 * (g2 ")) . x1 = (ff1 * (g1 ")) . x2 )
assume that
A86: x1 in dom (ff2 * (g2 ")) and
A87: x2 in (dom (ff1 * (g1 "))) \ (dom (ff2 * (g2 "))) ; :: thesis: not (ff2 * (g2 ")) . x1 = (ff1 * (g1 ")) . x2
A88: x1 in dom (g2 ") by ;
A89: (ff2 * (g2 ")) . x1 in P2 by ;
A90: x2 in dom (ff1 * (g1 ")) by ;
then A91: x2 in dom (g1 ") by FUNCT_1:11;
assume A92: (ff2 * (g2 ")) . x1 = (ff1 * (g1 ")) . x2 ; :: thesis: contradiction
then (ff2 * (g2 ")) . x1 in P1 by ;
then A93: (ff2 * (g2 ")) . x1 in P1 /\ P2 by ;
per cases ( (ff2 * (g2 ")) . x1 = p1 or (ff2 * (g2 ")) . x1 = p2 ) by ;
suppose A94: (ff2 * (g2 ")) . x1 = p1 ; :: thesis: contradiction
A95: (g1 ") . x2 in dom ff1 by ;
p1 = ff1 . ((g1 ") . x2) by ;
then A96: (g1 ") . x2 = 0 by ;
A97: p00 in dom (g2 ") by ;
A98: (g2 ") . x1 in dom ff2 by ;
p1 = ff2 . ((g2 ") . x1) by ;
then (g2 ") . x1 = 0 by ;
then A99: x1 = p00 by ;
p00 in dom (g1 ") by ;
then x2 in dom (ff2 * (g2 ")) by ;
hence contradiction by A87, XBOOLE_0:def 5; :: thesis: verum
end;
suppose A100: (ff2 * (g2 ")) . x1 = p2 ; :: thesis: contradiction
A101: (g1 ") . x2 in dom ff1 by ;
p2 = ff1 . ((g1 ") . x2) by ;
then A102: (g1 ") . x2 = 1 by ;
A103: p11 in dom (g2 ") by ;
A104: (g2 ") . x1 in dom ff2 by ;
p2 = ff2 . ((g2 ") . x1) by ;
then (g2 ") . x1 = 1 by ;
then A105: x1 = p11 by ;
p11 in dom (g1 ") by ;
then x2 in dom (ff2 * (g2 ")) by ;
hence contradiction by A87, XBOOLE_0:def 5; :: thesis: verum
end;
end;
end;
then A106: h is one-to-one by ;
A107: (TOP-REAL 2) | P9 is T_2 by TOPMETR:2;
A108: dom (ff2 * (g2 ")) = dom (g2 ") by ;
(ff1 * (g1 ")) .: ((dom (ff1 * (g1 "))) /\ (dom (ff2 * (g2 ")))) c= rng (ff2 * (g2 "))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (ff1 * (g1 ")) .: ((dom (ff1 * (g1 "))) /\ (dom (ff2 * (g2 ")))) or a in rng (ff2 * (g2 ")) )
A109: dom (ff2 * (g2 ")) = the carrier of (() | Lh2) by FUNCT_2:def 1;
assume a in (ff1 * (g1 ")) .: ((dom (ff1 * (g1 "))) /\ (dom (ff2 * (g2 ")))) ; :: thesis: a in rng (ff2 * (g2 "))
then A110: ex x being object st
( x in dom (ff1 * (g1 ")) & x in (dom (ff1 * (g1 "))) /\ (dom (ff2 * (g2 "))) & a = (ff1 * (g1 ")) . x ) by FUNCT_1:def 6;
dom (ff1 * (g1 ")) = the carrier of (() | Lh1) by FUNCT_2:def 1;
then ( a = p1 or a = p2 ) by ;
hence a in rng (ff2 * (g2 ")) by ; :: thesis: verum
end;
then A111: rng h = [#] (() | P9) by ;
reconsider h = h as Function of (),(() | P) ;
take h ; :: according to TOPREAL2:def 1 :: thesis:
(TOP-REAL 2) | RS is compact by ;
hence h is being_homeomorphism by ; :: thesis: verum