let n be Element of NAT ; :: thesis: for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & f is one-to-one & rng f = P & f . 0 = p1 & f . 1 = p2 )
let P be Subset of (TOP-REAL n); :: thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & f is one-to-one & rng f = P & f . 0 = p1 & f . 1 = p2 )
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( P is_an_arc_of p1,p2 implies ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & f is one-to-one & rng f = P & f . 0 = p1 & f . 1 = p2 ) )
assume A1: P is_an_arc_of p1,p2 ; :: thesis: ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & f is one-to-one & rng f = P & f . 0 = p1 & f . 1 = p2 )
then consider f2 being Function of I[01] ,((TOP-REAL n) | P) such that
A2: ( f2 is being_homeomorphism & f2 . 0 = p1 & f2 . 1 = p2 ) by TOPREAL1:def 2;
p1 in P by A1, TOPREAL1:4;
then consider g being Function of I[01] ,(TOP-REAL n) such that
A3: ( f2 = g & g is continuous & g is one-to-one ) by A2, JORDAN7:15;
rng g = [#] ((TOP-REAL n) | P) by A2, A3, TOPS_2:def 5
.= P by PRE_TOPC:def 10 ;
hence ex f being Function of I[01] ,(TOP-REAL n) st
( f is continuous & f is one-to-one & rng f = P & f . 0 = p1 & f . 1 = p2 ) by A2, A3; :: thesis: verum