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 t being Point of S holds dist ((In ((f . t),T)),(In ((g . t),T))) <= dist (f,g)
let T be non empty MetrSpace; :: thesis: for f, g being Point of (MetricSpace_of_ContinuousFunctions (S,T))
for t being Point of S holds dist ((In ((f . t),T)),(In ((g . t),T))) <= dist (f,g)
let a, b be Point of (MetricSpace_of_ContinuousFunctions (S,T)); :: thesis: for t being Point of S holds dist ((In ((a . t),T)),(In ((b . t),T))) <= dist (a,b)
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
A2: ( a = x & x is continuous ) ;
b in ContinuousFunctions (S,T) ;
then consider y being Function of S,(TopSpaceMetr T) such that
A3: ( b = y & y is continuous ) ;
consider Dist1 being RealMap of S such that
A4: ( ( 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, A2, A3;
A5: ( rng Dist1 <> {} & rng Dist1 is bounded_above & rng Dist1 is bounded_below ) by A2, A3, A4, Th9;
let t be Point of S; :: thesis: dist ((In ((a . t),T)),(In ((b . t),T))) <= dist (a,b)
A6: Dist1 . t = dist ((In ((x . t),T)),(In ((y . t),T))) by A4;
Dist1 . t in rng Dist1 by FUNCT_2:112;
hence dist ((In ((a . t),T)),(In ((b . t),T))) <= dist (a,b) by A6, A2, A3, A4, A5, SEQ_4:def 1; :: thesis: verum