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

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