let f be Function of I[01] ,(TOP-REAL 2); :: thesis: ( f is continuous & f is one-to-one implies ex f2 being Function of I[01] ,(TOP-REAL 2) st
( f2 . 0 = f . 1 & f2 . 1 = f . 0 & rng f2 = rng f & f2 is continuous & f2 is one-to-one ) )
assume A1: ( f is continuous & f is one-to-one ) ; :: thesis: ex f2 being Function of I[01] ,(TOP-REAL 2) st
( f2 . 0 = f . 1 & f2 . 1 = f . 0 & rng f2 = rng f & f2 is continuous & f2 is one-to-one )
A2: I[01] is compact by HEINE:11, TOPMETR:27;
A3: dom f = the carrier of I[01] by FUNCT_2:def 1;
then A4: f . 1 in rng f by Lm1, BORSUK_1:83, FUNCT_1:12;
reconsider P = rng f as non empty Subset of (TOP-REAL 2) by A3, Lm1, BORSUK_1:83, FUNCT_1:12;
consider f1 being Function of I[01] ,((TOP-REAL 2) | P) such that
A5: ( f1 = f & f1 is being_homeomorphism ) by A1, A2, JGRAPH_1:64;
f . 0 in rng f by A3, Lm1, BORSUK_1:83, FUNCT_1:12;
then reconsider p1 = f . 0 , p2 = f . 1 as Point of (TOP-REAL 2) by A4;
P is_an_arc_of p1,p2 by A5, TOPREAL1:def 2;
then P is_an_arc_of p2,p1 by JORDAN5B:14;
then consider f3 being Function of I[01] ,((TOP-REAL 2) | P) such that
A6: ( f3 is being_homeomorphism & f3 . 0 = p2 & f3 . 1 = p1 ) by TOPREAL1:def 2;
A7: rng f3 = [#] ((TOP-REAL 2) | P) by A6, TOPS_2:def 5
.= P by PRE_TOPC:def 10 ;
consider f4 being Function of I[01] ,(TOP-REAL 2) such that
A8: ( f3 = f4 & f4 is continuous & f4 is one-to-one ) by A6, JORDAN7:15;
thus ex f2 being Function of I[01] ,(TOP-REAL 2) st
( f2 . 0 = f . 1 & f2 . 1 = f . 0 & rng f2 = rng f & f2 is continuous & f2 is one-to-one ) by A6, A7, A8; :: thesis: verum