let n be Nat; :: thesis: for r being Real
for p, p1, p2 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 p, p1, p2 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 p, p1, p2 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 that
A1: ( f is continuous & f . 0 = p1 & f . 1 = p2 ) and
A2: ( 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:9;
then consider f1 being Function of I[01],((TOP-REAL n) | (LSeg (p2,p))) such that
A3: f1 is being_homeomorphism and
A4: ( f1 . 0 = p2 & f1 . 1 = p ) by TOPREAL1:def 1;
reconsider f2 = f1 as Function of I[01],(TOP-REAL n) by JORDAN6:3;
rng f1 = [#] ((TOP-REAL n) | (LSeg (p2,p))) by A3;
then rng f2 = LSeg (p2,p) by PRE_TOPC:def 5;
then A5: (rng f) \/ (rng f2) c= (rng f) \/ (Ball (u,r)) by A2, TOPREAL3:21, XBOOLE_1:9;
f1 is continuous by A3;
then f2 is continuous by JORDAN6:3;
then ex h3 being Function of I[01],(TOP-REAL n) st
( h3 is continuous & p1 = h3 . 0 & p = h3 . 1 & rng h3 c= (rng f) \/ (rng f2) ) by A1, A4, BORSUK_2:13;
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 A5, 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;