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 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 p1, p2, p 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 p1, p2, p 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 that
A1: f is continuous and
A2: rng f c= P and
A3: ( f . 0 = p1 & f . 1 = p2 ) and
A4: p in Ball u,r and
A5: p2 in Ball u,r and
A6: 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 )
consider f3 being Function of I[01] ,(TOP-REAL n) such that
A7: ( f3 is continuous & f3 . 0 = p1 & f3 . 1 = p & rng f3 c= (rng f) \/ (Ball u,r) ) by A1, A3, A4, A5, Th81;
(rng f) \/ (Ball u,r) c= P by A2, A6, 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 A7, XBOOLE_1:1; :: thesis: verum