let n be Element of NAT ; :: thesis:
let a, p1, p2 be Point of (TOP-REAL n); :: thesis:
let P be Subset of (TOP-REAL n); :: thesis:
assume A1: a in P ; :: thesis:
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 2 :: thesis:
rng f = [#] ((TOP-REAL n) | P) by A2, TOPS_2:def 5
.= the carrier of ((TOP-REAL n) | P)
.= P by PRE_TOPC:29 ;
then consider r being set such that
A4: r in dom f and
A5: a = f . r by A1, FUNCT_1:def 5;
A6: dom f = [#] I[01] by A2, TOPS_2:def 5
.= [.0 ,1.] by BORSUK_1:83 ;
then reconsider r = r as Real by A4;
take f ; :: thesis:
take r ; :: thesis:
thus ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by A2, A3; :: thesis:
thus ( 0 <= r & r <= 1 ) by A4, A6, XXREAL_1:1; :: thesis:
thus f . r = a by A5; :: thesis: