let A be Subset of (); :: thesis: for p1, p2 being Point of () st A is_an_arc_of p1,p2 holds
ex g being Function of I,() st
( g is continuous & g is one-to-one & rng g = A & g . 0 = p1 & g . 1 = p2 )

let p1, p2 be Point of (); :: thesis: ( A is_an_arc_of p1,p2 implies ex g being Function of I,() 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,() 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 () by TOPREAL1:1;
consider f being Function of I,(() | A9) such that
A2: f is being_homeomorphism and
A3: ( f . 0 = p1 & f . 1 = p2 ) by ;
consider g being Function of I,() such that
A4: f = g and
A5: ( g is continuous & g is one-to-one ) by ;
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 = [#] (() | A9) by ;
hence rng g = A by ; :: thesis: ( g . 0 = p1 & g . 1 = p2 )
thus ( g . 0 = p1 & g . 1 = p2 ) by A3, A4; :: thesis: verum