let n be Element of NAT ; :: thesis: for P being Subset of ()
for Q being non empty Subset of ()
for g being Function of I,(() | P)
for f being Function of (),(() | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous

let P be Subset of (); :: thesis: for Q being non empty Subset of ()
for g being Function of I,(() | P)
for f being Function of (),(() | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous

let Q be non empty Subset of (); :: thesis: for g being Function of I,(() | P)
for f being Function of (),(() | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous

let g be Function of I,(() | P); :: thesis: for f being Function of (),(() | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous

let f be Function of (),(() | 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:
(TOP-REAL n) | P = TopSpaceMetr (() | Q) by ;
hence f is uniformly_continuous by ; :: thesis: verum