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 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:15;
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 2;
reconsider f2 = f1 as Function of I[01] ,(TOP-REAL n) by JORDAN6:4;
rng f1 = [#] ((TOP-REAL n) | (LSeg p2,p)) by A3, TOPS_2:def 5;
then rng f2 = LSeg p2,p by PRE_TOPC:def 10;
then A5: (rng f) \/ (rng f2) c= (rng f) \/ (Ball u,r) by A2, TOPREAL3:28, XBOOLE_1:9;
f1 is continuous by A3, TOPS_2:def 5;
then f2 is continuous by JORDAN6:4;
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:16;
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;