let Dp be non empty Subset of (TOP-REAL 2); :: thesis: for f being Function of ((TOP-REAL 2) | Dp),I(01)
for C being non empty Subset of (TOP-REAL 2) st f is being_homeomorphism & C c= Dp & ex p1, p2 being Point of I[01] st
( p1 < p2 & f .: C = [.p1,p2.] ) holds
ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2
let f be Function of ((TOP-REAL 2) | Dp),I(01); :: thesis: for C being non empty Subset of (TOP-REAL 2) st f is being_homeomorphism & C c= Dp & ex p1, p2 being Point of I[01] st
( p1 < p2 & f .: C = [.p1,p2.] ) holds
ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2
let C be non empty Subset of (TOP-REAL 2); :: thesis: ( f is being_homeomorphism & C c= Dp & ex p1, p2 being Point of I[01] st
( p1 < p2 & f .: C = [.p1,p2.] ) implies ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2 )
assume that
A1: f is being_homeomorphism and
A2: C c= Dp ; :: thesis: ( for p1, p2 being Point of I[01] holds
( not p1 < p2 or not f .: C = [.p1,p2.] ) or ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2 )
reconsider C9 = C as Subset of ((TOP-REAL 2) | Dp) by A2, PRE_TOPC:8;
A3: the carrier of ((TOP-REAL 2) | Dp) = Dp by PRE_TOPC:8;
dom f = the carrier of ((TOP-REAL 2) | Dp) by FUNCT_2:def 1;
then C c= dom f by A2, PRE_TOPC:8;
then A4: C c= f " (f .: C) by FUNCT_1:76;
given p1, p2 being Point of I[01] such that A5: p1 < p2 and
A6: f .: C = [.p1,p2.] ; :: thesis: ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2
reconsider E = [.p1,p2.] as Subset of I(01) by A6;
A7: rng f = [#] I(01) by A1, TOPS_2:def 5;
A8: ( f is continuous & f is one-to-one ) by A1, TOPS_2:def 5;
then f " (f .: C) c= C by FUNCT_1:82;
then f " (f .: C) = C by A4, XBOOLE_0:def 10;
then A9: (f ") .: E = C by A6, A8, A7, TOPS_2:55;
the carrier of ((TOP-REAL 2) | C) = C by PRE_TOPC:8;
then A10: (TOP-REAL 2) | C is SubSpace of (TOP-REAL 2) | Dp by A2, A3, TOPMETR:3;
set g = (f ") | E;
the carrier of (I(01) | E) = E by PRE_TOPC:8;
then A11: (f ") | E is Function of the carrier of (I(01) | E), the carrier of ((TOP-REAL 2) | Dp) by FUNCT_2:32;
A12: rng ((f ") | E) = (f ") .: E by RELAT_1:115
.= [#] ((TOP-REAL 2) | C) by A9, PRE_TOPC:8 ;
then reconsider g = (f ") | E as Function of (I(01) | E),((TOP-REAL 2) | C) by A11, FUNCT_2:6;
f " is being_homeomorphism by A1, TOPS_2:56;
then A13: f " is one-to-one by TOPS_2:def 5;
then A14: g is one-to-one by FUNCT_1:52;
A15: f is onto by A7, FUNCT_2:def 3;
g is onto by A12, FUNCT_2:def 3;
then A16: g " = g " by A14, TOPS_2:def 4
.= ((f ") ") | ((f ") .: E) by A13, RFUNCT_2:17
.= ((f ") ") | ((f ") .: E) by A8, A15, TOPS_2:def 4
.= f | C by A8, A9, FUNCT_1:43 ;
then reconsider t = f | C as Function of ((TOP-REAL 2) | C),(I(01) | E) ;
dom (f ") = the carrier of I(01) by FUNCT_2:def 1;
then dom g = E by RELAT_1:62
.= the carrier of (I(01) | E) by PRE_TOPC:8 ;
then A17: dom g = [#] (I(01) | E) ;
f " is continuous by A1, TOPS_2:def 5;
then A18: g is continuous by A10, Th41;
((TOP-REAL 2) | Dp) | C9 = (TOP-REAL 2) | C by A2, PRE_TOPC:7;
then t is continuous by A8, Th41;
then g is being_homeomorphism by A12, A17, A14, A18, A16, TOPS_2:def 5;
then I(01) | E,(TOP-REAL 2) | C are_homeomorphic by T_0TOPSP:def 1;
hence ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2 by A5, Th51; :: thesis: verum