let n be Element of NAT ; :: thesis: for p1, p2 being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
ex F being Path of p1,p2 ex f being Function of I[01] ,((TOP-REAL n) | P) st
( rng f = P & F = f )
let p1, p2 be Point of (TOP-REAL n); :: thesis: for P being Subset of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
ex F being Path of p1,p2 ex f being Function of I[01] ,((TOP-REAL n) | P) st
( rng f = P & F = f )
let P be Subset of (TOP-REAL n); :: thesis: ( P is_an_arc_of p1,p2 implies ex F being Path of p1,p2 ex f being Function of I[01] ,((TOP-REAL n) | P) st
( rng f = P & F = f ) )
assume A1: P is_an_arc_of p1,p2 ; :: thesis: ex F being Path of p1,p2 ex f being Function of I[01] ,((TOP-REAL n) | P) st
( rng f = P & F = f )
then reconsider P1 = P as non empty Subset of (TOP-REAL n) by TOPREAL1:4;
consider h being Function of I[01] ,((TOP-REAL n) | P) such that
A2: h is being_homeomorphism and
A3: ( h . 0 = p1 & h . 1 = p2 ) by A1, TOPREAL1:def 2;
h is Function of I[01] ,((TOP-REAL n) | P1) ;
then reconsider h1 = h as Function of I[01] ,(TOP-REAL n) by TOPREALA:28;
h1 is Path of p1,p2

proof

h is continuous by A2;
hence ( h1 is continuous & h1 . 0 = p1 & h1 . 1 = p2 ) by A3, PRE_TOPC:56; :: according to BORSUK_2:def 4 :: thesis: verum

end;

then reconsider f = h as Path of p1,p2 ;
take f ; :: thesis: ex f being Function of I[01] ,((TOP-REAL n) | P) st
( rng f = P & f = f )
take h ; :: thesis: ( rng h = P & f = h )
thus rng h = [#] ((TOP-REAL n) | P) by A2, TOPS_2:def 5
.= P by PRE_TOPC:29 ; :: thesis: f = h
thus f = h ; :: thesis: verum