let n be Element of NAT ; :: thesis: for P being Subset of (TOP-REAL n)
for Q being non empty Subset of (Euclid n)
for g being Function of I[01] ,((TOP-REAL n) | P)
for f being Function of (Closed-Interval-MSpace 0 ,1),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous
let P be Subset of (TOP-REAL n); :: thesis: for Q being non empty Subset of (Euclid n)
for g being Function of I[01] ,((TOP-REAL n) | P)
for f being Function of (Closed-Interval-MSpace 0 ,1),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous
let Q be non empty Subset of (Euclid n); :: thesis: for g being Function of I[01] ,((TOP-REAL n) | P)
for f being Function of (Closed-Interval-MSpace 0 ,1),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous
let g be Function of I[01] ,((TOP-REAL n) | P); :: thesis: for f being Function of (Closed-Interval-MSpace 0 ,1),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous
let f be Function of (Closed-Interval-MSpace 0 ,1),((Euclid n) | Q); :: thesis: ( P = Q & g is continuous & f = g implies f is uniformly_continuous )
assume A1: ( P = Q & g is continuous & f = g ) ; :: thesis: f is uniformly_continuous
then (TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q) by EUCLID:67;
hence f is uniformly_continuous by A1, Lm1, Th8, TOPMETR:27; :: thesis: verum