let n be Element of NAT ; :: thesis: for a, p1, p2 being Point of ()
for P being Subset of () st a in P & P is_an_arc_of p1,p2 holds
ex f being Function of I,(() | P) ex r being Real st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a )

let a, p1, p2 be Point of (); :: thesis: for P being Subset of () st a in P & P is_an_arc_of p1,p2 holds
ex f being Function of I,(() | P) ex r being Real st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a )

let P be Subset of (); :: thesis: ( a in P & P is_an_arc_of p1,p2 implies ex f being Function of I,(() | P) ex r being Real st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a ) )

assume A1: a in P ; :: thesis: ( not P is_an_arc_of p1,p2 or ex f being Function of I,(() | P) ex r being Real st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a ) )

given f being Function of I,(() | P) such that A2: f is being_homeomorphism and
A3: ( f . 0 = p1 & f . 1 = p2 ) ; :: according to TOPREAL1:def 1 :: thesis: ex f being Function of I,(() | P) ex r being Real st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a )

rng f = [#] (() | P) by
.= the carrier of (() | P)
.= P by PRE_TOPC:8 ;
then consider r being object such that
A4: r in dom f and
A5: a = f . r by ;
A6: dom f = [#] I by
.= [.0,1.] by BORSUK_1:40 ;
then reconsider r = r as Real by A4;
take f ; :: thesis: ex r being Real st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a )

take r ; :: thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a )
thus ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by A2, A3; :: thesis: ( 0 <= r & r <= 1 & f . r = a )
thus ( 0 <= r & r <= 1 ) by ; :: thesis: f . r = a
thus f . r = a by A5; :: thesis: verum