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

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