let n be Element of NAT ; :: thesis: for g being Function of I[01],(TOP-REAL n)
for f being Function of (Closed-Interval-MSpace (0,1)),(Euclid n) st g is continuous & f = g holds
f is uniformly_continuous
let g be Function of I[01],(TOP-REAL n); :: thesis: for f being Function of (Closed-Interval-MSpace (0,1)),(Euclid n) st g is continuous & f = g holds
f is uniformly_continuous
let f be Function of (Closed-Interval-MSpace (0,1)),(Euclid n); :: thesis: ( g is continuous & f = g implies f is uniformly_continuous )
assume that
A1: g is continuous and
A2: f = g ; :: thesis: f is uniformly_continuous
A3: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider h = g as Function of I[01],(TopSpaceMetr (Euclid n)) ;
h is continuous by A1, A3, PRE_TOPC:33;
hence f is uniformly_continuous by A2, Lm1, Th7, TOPMETR:20; :: thesis: verum