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 that

A1: P = Q and

A2: ( g is continuous & f = g ) ; :: thesis: f is uniformly_continuous

(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q) by A1, EUCLID:63;

hence f is uniformly_continuous by A2, Lm1, Th7, TOPMETR:20; :: thesis: verum

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 that

A1: P = Q and

A2: ( g is continuous & f = g ) ; :: thesis: f is uniformly_continuous

(TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q) by A1, EUCLID:63;

hence f is uniformly_continuous by A2, Lm1, Th7, TOPMETR:20; :: thesis: verum