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 ) )
A1: I[01] is compact by HEINE:4, TOPMETR:20;
A2: dom f = the carrier of I[01] by FUNCT_2:def 1;
then reconsider P = rng f as non empty Subset of (TOP-REAL 2) by Lm1, BORSUK_1:40, FUNCT_1:3;
( f . 1 in rng f & f . 0 in rng f ) by A2, Lm1, Lm2, BORSUK_1:40, FUNCT_1:3;
then reconsider p1 = f . 0, p2 = f . 1 as Point of (TOP-REAL 2) ;
assume ( 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 )
then ex f1 being Function of I[01],((TOP-REAL 2) | P) st
( f1 = f & f1 is being_homeomorphism ) by A1, JGRAPH_1:46;
then P is_an_arc_of p1,p2 by TOPREAL1:def 1;
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
A3: f3 is being_homeomorphism and
A4: ( f3 . 0 = p2 & f3 . 1 = p1 ) by TOPREAL1:def 1;
A5: ex f4 being Function of I[01],(TOP-REAL 2) st
( f3 = f4 & f4 is continuous & f4 is one-to-one ) by A3, JORDAN7:15;
rng f3 = [#] ((TOP-REAL 2) | P) by A3, TOPS_2:def 5
.= P by PRE_TOPC:def 5 ;
hence 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 A4, A5; :: thesis: verum