let n be Element of NAT ; :: thesis: for a, p1, p2 being Point of (TOP-REAL n)

for P being Subset of (TOP-REAL n) st a in P & P is_an_arc_of p1,p2 holds

ex f being Function of I[01],((TOP-REAL n) | 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 (TOP-REAL n); :: thesis: for P being Subset of (TOP-REAL n) st a in P & P is_an_arc_of p1,p2 holds

ex f being Function of I[01],((TOP-REAL n) | 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 (TOP-REAL n); :: thesis: ( a in P & P is_an_arc_of p1,p2 implies ex f being Function of I[01],((TOP-REAL n) | 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[01],((TOP-REAL n) | 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[01],((TOP-REAL n) | 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[01],((TOP-REAL n) | 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 = [#] ((TOP-REAL n) | P) by A2, TOPS_2:def 5

.= the carrier of ((TOP-REAL n) | P)

.= P by PRE_TOPC:8 ;

then consider r being object such that

A4: r in dom f and

A5: a = f . r by A1, FUNCT_1:def 3;

A6: dom f = [#] I[01] by A2, TOPS_2:def 5

.= [.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 A4, A6, XXREAL_1:1; :: thesis: f . r = a

thus f . r = a by A5; :: thesis: verum

for P being Subset of (TOP-REAL n) st a in P & P is_an_arc_of p1,p2 holds

ex f being Function of I[01],((TOP-REAL n) | 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 (TOP-REAL n); :: thesis: for P being Subset of (TOP-REAL n) st a in P & P is_an_arc_of p1,p2 holds

ex f being Function of I[01],((TOP-REAL n) | 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 (TOP-REAL n); :: thesis: ( a in P & P is_an_arc_of p1,p2 implies ex f being Function of I[01],((TOP-REAL n) | 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[01],((TOP-REAL n) | 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[01],((TOP-REAL n) | 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[01],((TOP-REAL n) | 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 = [#] ((TOP-REAL n) | P) by A2, TOPS_2:def 5

.= the carrier of ((TOP-REAL n) | P)

.= P by PRE_TOPC:8 ;

then consider r being object such that

A4: r in dom f and

A5: a = f . r by A1, FUNCT_1:def 3;

A6: dom f = [#] I[01] by A2, TOPS_2:def 5

.= [.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 A4, A6, XXREAL_1:1; :: thesis: f . r = a

thus f . r = a by A5; :: thesis: verum