let S be non empty compact TopSpace; :: thesis: for T being non empty MetrSpace
for f, g being Point of (MetricSpace_of_ContinuousFunctions (S,T))
for f1, g1 being Function of S,T
for e being Real st f = f1 & g = g1 & ( for t being Point of S holds dist ((f1 . t),(g1 . t)) <= e ) holds
dist (f,g) <= e
let T be non empty MetrSpace; :: thesis: for f, g being Point of (MetricSpace_of_ContinuousFunctions (S,T))
for f1, g1 being Function of S,T
for e being Real st f = f1 & g = g1 & ( for t being Point of S holds dist ((f1 . t),(g1 . t)) <= e ) holds
dist (f,g) <= e
let a, b be Point of (MetricSpace_of_ContinuousFunctions (S,T)); :: thesis: for f1, g1 being Function of S,T
for e being Real st a = f1 & b = g1 & ( for t being Point of S holds dist ((f1 . t),(g1 . t)) <= e ) holds
dist (a,b) <= e
let f1, g1 be Function of S,T; :: thesis: for e being Real st a = f1 & b = g1 & ( for t being Point of S holds dist ((f1 . t),(g1 . t)) <= e ) holds
dist (a,b) <= e
let e be Real; :: thesis: ( a = f1 & b = g1 & ( for t being Point of S holds dist ((f1 . t),(g1 . t)) <= e ) implies dist (a,b) <= e )
assume A1: ( a = f1 & b = g1 & ( for t being Point of S holds dist ((f1 . t),(g1 . t)) <= e ) ) ; :: thesis: dist (a,b) <= e
set M = MetricSpace_of_ContinuousFunctions (S,T);
set A = ContinuousFunctions (S,T);
reconsider f = the distance of (MetricSpace_of_ContinuousFunctions (S,T)) as Function of [:(ContinuousFunctions (S,T)),(ContinuousFunctions (S,T)):],REAL ;
a in ContinuousFunctions (S,T) ;
then consider x being Function of S,(TopSpaceMetr T) such that
A3: ( a = x & x is continuous ) ;
b in ContinuousFunctions (S,T) ;
then consider y being Function of S,(TopSpaceMetr T) such that
A4: ( b = y & y is continuous ) ;
consider Dist1 being RealMap of S such that
A5: ( ( for t being Point of S holds Dist1 . t = dist ((In ((x . t),T)),(In ((y . t),T))) ) & f . (a,b) = upper_bound (rng Dist1) ) by Def5, A3, A4;
A6: ( rng Dist1 <> {} & rng Dist1 is bounded_above & rng Dist1 is bounded_below ) by A3, A4, A5, Th9;

now :: thesis: for r being Real st r in rng Dist1 holds
r <= e

let r be Real; :: thesis: ( r in rng Dist1 implies r <= e )
assume r in rng Dist1 ; :: thesis: r <= e
then consider t being Element of S such that
A7: r = Dist1 . t by FUNCT_2:113;
Dist1 . t = dist ((In ((x . t),T)),(In ((y . t),T))) by A5;
hence r <= e by A7, A1, A3, A4; :: thesis: verum

end;

hence dist (a,b) <= e by A6, SEQ_4:45, A5; :: thesis: verum