let n be Nat; :: thesis: for r being Real
for p, q being Point of (TOP-REAL n)
for u being Point of (Euclid n) st p <> q & p in Ball (u,r) & q in Ball (u,r) holds
ex h being Function of I[01],(TOP-REAL n) st
( h is continuous & h . 0 = p & h . 1 = q & rng h c= Ball (u,r) )
let r be Real; :: thesis: for p, q being Point of (TOP-REAL n)
for u being Point of (Euclid n) st p <> q & p in Ball (u,r) & q in Ball (u,r) holds
ex h being Function of I[01],(TOP-REAL n) st
( h is continuous & h . 0 = p & h . 1 = q & rng h c= Ball (u,r) )
let p, q be Point of (TOP-REAL n); :: thesis: for u being Point of (Euclid n) st p <> q & p in Ball (u,r) & q in Ball (u,r) holds
ex h being Function of I[01],(TOP-REAL n) st
( h is continuous & h . 0 = p & h . 1 = q & rng h c= Ball (u,r) )
let u be Point of (Euclid n); :: thesis: ( p <> q & p in Ball (u,r) & q in Ball (u,r) implies ex h being Function of I[01],(TOP-REAL n) st
( h is continuous & h . 0 = p & h . 1 = q & rng h c= Ball (u,r) ) )
assume that
A1: p <> q and
A2: ( p in Ball (u,r) & q in Ball (u,r) ) ; :: thesis: ex h being Function of I[01],(TOP-REAL n) st
( h is continuous & h . 0 = p & h . 1 = q & rng h c= Ball (u,r) )
reconsider Q = Ball (u,r) as Subset of (TOP-REAL n) by TOPREAL3:8;
Q is convex by Th55;
then A3: LSeg (p,q) c= Ball (u,r) by A2, JORDAN1:def 1;
reconsider P = LSeg (p,q) as Subset of (TOP-REAL n) ;
LSeg (p,q) is_an_arc_of p,q by A1, TOPREAL1:9;
then consider f being Function of I[01],((TOP-REAL n) | P) such that
A4: f is being_homeomorphism and
A5: ( f . 0 = p & f . 1 = q ) by TOPREAL1:def 1;
reconsider h = f as Function of I[01],(TOP-REAL n) by JORDAN6:3;
take h ; :: thesis: ( h is continuous & h . 0 = p & h . 1 = q & rng h c= Ball (u,r) )
( rng f = [#] ((TOP-REAL n) | P) & f is continuous ) by A4;
hence ( h is continuous & h . 0 = p & h . 1 = q & rng h c= Ball (u,r) ) by A3, A5, JORDAN6:3, PRE_TOPC:def 5; :: thesis: verum