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 P being Subset of (TOP-REAL n)
for f being Function of I[01],(TOP-REAL n) st f is continuous & rng f c= P & f . 0 = p1 & f . 1 = p2 & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= P holds
ex f1 being Function of I[01],(TOP-REAL n) st
( f1 is continuous & rng f1 c= P & f1 . 0 = p1 & f1 . 1 = p )
let r be Real; :: thesis: for p, p1, p2 being Point of (TOP-REAL n)
for u being Point of (Euclid n)
for P being Subset of (TOP-REAL n)
for f being Function of I[01],(TOP-REAL n) st f is continuous & rng f c= P & f . 0 = p1 & f . 1 = p2 & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= P holds
ex f1 being Function of I[01],(TOP-REAL n) st
( f1 is continuous & rng f1 c= P & f1 . 0 = p1 & f1 . 1 = p )
let p, p1, p2 be Point of (TOP-REAL n); :: thesis: for u being Point of (Euclid n)
for P being Subset of (TOP-REAL n)
for f being Function of I[01],(TOP-REAL n) st f is continuous & rng f c= P & f . 0 = p1 & f . 1 = p2 & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= P holds
ex f1 being Function of I[01],(TOP-REAL n) st
( f1 is continuous & rng f1 c= P & f1 . 0 = p1 & f1 . 1 = p )
let u be Point of (Euclid n); :: thesis: for P being Subset of (TOP-REAL n)
for f being Function of I[01],(TOP-REAL n) st f is continuous & rng f c= P & f . 0 = p1 & f . 1 = p2 & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= P holds
ex f1 being Function of I[01],(TOP-REAL n) st
( f1 is continuous & rng f1 c= P & f1 . 0 = p1 & f1 . 1 = p )
let P be Subset of (TOP-REAL n); :: thesis: for f being Function of I[01],(TOP-REAL n) st f is continuous & rng f c= P & f . 0 = p1 & f . 1 = p2 & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= P holds
ex f1 being Function of I[01],(TOP-REAL n) st
( f1 is continuous & rng f1 c= P & f1 . 0 = p1 & f1 . 1 = p )
let f be Function of I[01],(TOP-REAL n); :: thesis: ( f is continuous & rng f c= P & f . 0 = p1 & f . 1 = p2 & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= P implies ex f1 being Function of I[01],(TOP-REAL n) st
( f1 is continuous & rng f1 c= P & f1 . 0 = p1 & f1 . 1 = p ) )
assume ( f is continuous & rng f c= P & f . 0 = p1 & f . 1 = p2 & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= P ) ; :: thesis: ex f1 being Function of I[01],(TOP-REAL n) st
( f1 is continuous & rng f1 c= P & f1 . 0 = p1 & f1 . 1 = p )
then ( ex f3 being Function of I[01],(TOP-REAL n) st
( f3 is continuous & f3 . 0 = p1 & f3 . 1 = p & rng f3 c= (rng f) \/ (Ball (u,r)) ) & (rng f) \/ (Ball (u,r)) c= P ) by Th57, XBOOLE_1:8;
hence ex f1 being Function of I[01],(TOP-REAL n) st
( f1 is continuous & rng f1 c= P & f1 . 0 = p1 & f1 . 1 = p ) by XBOOLE_1:1; :: thesis: verum