let A be Subset of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 holds
ex g being Function of I[01],(TOP-REAL 2) st
( g is continuous & g is one-to-one & rng g = A & g . 0 = p1 & g . 1 = p2 )
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( A is_an_arc_of p1,p2 implies ex g being Function of I[01],(TOP-REAL 2) st
( g is continuous & g is one-to-one & rng g = A & g . 0 = p1 & g . 1 = p2 ) )
assume A1: A is_an_arc_of p1,p2 ; :: thesis: ex g being Function of I[01],(TOP-REAL 2) st
( g is continuous & g is one-to-one & rng g = A & g . 0 = p1 & g . 1 = p2 )
then reconsider A9 = A as non empty Subset of (TOP-REAL 2) by TOPREAL1:1;
consider f being Function of I[01],((TOP-REAL 2) | A9) such that
A2: f is being_homeomorphism and
A3: ( f . 0 = p1 & f . 1 = p2 ) by A1, TOPREAL1:def 1;
consider g being Function of I[01],(TOP-REAL 2) such that
A4: f = g and
A5: ( g is continuous & g is one-to-one ) by A2, Th15;
take g ; :: thesis: ( g is continuous & g is one-to-one & rng g = A & g . 0 = p1 & g . 1 = p2 )
thus ( g is continuous & g is one-to-one ) by A5; :: thesis: ( rng g = A & g . 0 = p1 & g . 1 = p2 )
rng f = [#] ((TOP-REAL 2) | A9) by A2, TOPS_2:def 5;
hence rng g = A by A4, PRE_TOPC:def 5; :: thesis: ( g . 0 = p1 & g . 1 = p2 )
thus ( g . 0 = p1 & g . 1 = p2 ) by A3, A4; :: thesis: verum