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 A' = A as non empty Subset of (TOP-REAL 2) by TOPREAL1:4;
consider f being Function of I[01] ,((TOP-REAL 2) | A') such that
A2: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by A1, TOPREAL1:def 2;
A3: rng f = [#] ((TOP-REAL 2) | A') by A2, TOPS_2:def 5;
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 )
thus rng g = A by A3, A4, PRE_TOPC:def 10; :: thesis: ( g . 0 = p1 & g . 1 = p2 )
thus ( g . 0 = p1 & g . 1 = p2 ) by A2, A4; :: thesis: verum