let n be Element of NAT ; 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); 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); ( 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
; ( 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 )
; TOPREAL1:def 1 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
; ex r being Real st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a )
take
r
; ( 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; ( 0 <= r & r <= 1 & f . r = a )
thus
( 0 <= r & r <= 1 )
by A4, A6, XXREAL_1:1; f . r = a
thus
f . r = a
by A5; verum