let f be Function of I[01],(TOP-REAL 2); ( 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 )
; 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; verum