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 and
A3: f2 . 0 = p1 and
A4: f2 . 1 = p2 by TOPREAL1:def 1;
p1 in P by A1, TOPREAL1:1;
then consider g being Function of I[01],(TOP-REAL n) such that
A5: f2 = g and
A6: g is continuous and
A7: g is one-to-one by A2, JORDAN7:15;
rng g = [#] ((TOP-REAL n) | P) by A2, A5, TOPS_2:def 5
.= P by PRE_TOPC:def 5 ;
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 A3, A4, A5, A6, A7; :: thesis: verum