let n be Element of NAT ; :: thesis: for r being Real
for p1, p2, p being Point of (TOP-REAL n)
for u being Point of (Euclid n)
for f being Function of I[01] ,(TOP-REAL n) st f is continuous & f . 0 = p1 & f . 1 = p2 & p in Ball u,r & p2 in Ball u,r holds
ex h being Function of I[01] ,(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball u,r) )

let r be Real; :: thesis: for p1, p2, p being Point of (TOP-REAL n)
for u being Point of (Euclid n)
for f being Function of I[01] ,(TOP-REAL n) st f is continuous & f . 0 = p1 & f . 1 = p2 & p in Ball u,r & p2 in Ball u,r holds
ex h being Function of I[01] ,(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball u,r) )

let p1, p2, p be Point of (TOP-REAL n); :: thesis: for u being Point of (Euclid n)
for f being Function of I[01] ,(TOP-REAL n) st f is continuous & f . 0 = p1 & f . 1 = p2 & p in Ball u,r & p2 in Ball u,r holds
ex h being Function of I[01] ,(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball u,r) )

let u be Point of (Euclid n); :: thesis: for f being Function of I[01] ,(TOP-REAL n) st f is continuous & f . 0 = p1 & f . 1 = p2 & p in Ball u,r & p2 in Ball u,r holds
ex h being Function of I[01] ,(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball u,r) )

let f be Function of I[01] ,(TOP-REAL n); :: thesis: ( f is continuous & f . 0 = p1 & f . 1 = p2 & p in Ball u,r & p2 in Ball u,r implies ex h being Function of I[01] ,(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball u,r) ) )

assume A1: ( f is continuous & f . 0 = p1 & f . 1 = p2 & p in Ball u,r & p2 in Ball u,r ) ; :: thesis: ex h being Function of I[01] ,(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball u,r) )

per cases ( p2 <> p or p2 = p ) ;
suppose p2 <> p ; :: thesis: ex h being Function of I[01] ,(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball u,r) )

then LSeg p2,p is_an_arc_of p2,p by TOPREAL1:15;
then consider f1 being Function of I[01] ,((TOP-REAL n) | (LSeg p2,p)) such that
A2: ( f1 is being_homeomorphism & f1 . 0 = p2 & f1 . 1 = p ) by TOPREAL1:def 2;
A3: ( dom f1 = [#] I[01] & rng f1 = [#] ((TOP-REAL n) | (LSeg p2,p)) & f1 is one-to-one & f1 is continuous & f1 " is continuous ) by A2, TOPS_2:def 5;
reconsider f2 = f1 as Function of I[01] ,(TOP-REAL n) by JORDAN6:4;
A4: f2 is continuous by A3, JORDAN6:4;
A5: rng f2 = LSeg p2,p by A3, PRE_TOPC:def 10;
consider h3 being Function of I[01] ,(TOP-REAL n) such that
A6: ( h3 is continuous & p1 = h3 . 0 & p = h3 . 1 & rng h3 c= (rng f) \/ (rng f2) ) by A1, A2, A4, BORSUK_2:16;
(rng f) \/ (rng f2) c= (rng f) \/ (Ball u,r) by A1, A5, TOPREAL3:28, XBOOLE_1:9;
hence ex h being Function of I[01] ,(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball u,r) ) by A6, XBOOLE_1:1; :: thesis: verum
end;
suppose p2 = p ; :: thesis: ex h being Function of I[01] ,(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball u,r) )

hence ex h being Function of I[01] ,(TOP-REAL n) st
( h is continuous & h . 0 = p1 & h . 1 = p & rng h c= (rng f) \/ (Ball u,r) ) by A1, XBOOLE_1:7; :: thesis: verum
end;
end;