let S be non empty compact TopSpace; :: thesis: for T being non empty MetrSpace holds
( MetricSpace_of_ContinuousFunctions (S,T) is Reflexive & MetricSpace_of_ContinuousFunctions (S,T) is discerning & MetricSpace_of_ContinuousFunctions (S,T) is symmetric & MetricSpace_of_ContinuousFunctions (S,T) is triangle )
let T be non empty MetrSpace; :: thesis: ( MetricSpace_of_ContinuousFunctions (S,T) is Reflexive & MetricSpace_of_ContinuousFunctions (S,T) is discerning & MetricSpace_of_ContinuousFunctions (S,T) is symmetric & MetricSpace_of_ContinuousFunctions (S,T) is triangle )
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 ;
for a being Element of ContinuousFunctions (S,T) holds f . (a,a) = 0

proof

let a be Element of ContinuousFunctions (S,T); :: thesis: f . (a,a) = 0
a in ContinuousFunctions (S,T) ;
then consider x being Function of S,(TopSpaceMetr T) such that
A2: ( a = x & x is continuous ) ;
consider Dist being RealMap of S such that
A3: ( ( for t being Point of S holds Dist . t = dist ((In ((x . t),T)),(In ((x . t),T))) ) & f . (a,a) = upper_bound (rng Dist) ) by Def5, A2;
for s being object holds
( s in rng Dist iff s in {0} )

proof

let s be object ; :: thesis: ( s in rng Dist iff s in {0} )

hereby :: thesis: ( s in {0} implies s in rng Dist )

assume s in rng Dist ; :: thesis: s in {0}
then consider t being Element of S such that
A4: s = Dist . t by FUNCT_2:113;
s = dist ((In ((x . t),T)),(In ((x . t),T))) by A3, A4
.= 0 by METRIC_1:1 ;
hence s in {0} by TARSKI:def 1; :: thesis: verum

end;

assume s in {0} ; :: thesis: s in rng Dist
then A5: s = 0 by TARSKI:def 1;
set t = the Point of S;
Dist . the Point of S = dist ((In ((x . the Point of S),T)),(In ((x . the Point of S),T))) by A3
.= s by A5, METRIC_1:1 ;
hence s in rng Dist by FUNCT_2:112; :: thesis: verum

end;

then rng Dist = {0} ;
hence f . (a,a) = 0 by SEQ_4:9, A3; :: thesis: verum

end;

then A6: f is Reflexive ;
for a, b being Element of ContinuousFunctions (S,T) st f . (a,b) = 0 holds
a = b

proof

let a, b be Element of ContinuousFunctions (S,T); :: thesis: ( f . (a,b) = 0 implies a = b )
assume A7: f . (a,b) = 0 ; :: thesis: a = b
a in ContinuousFunctions (S,T) ;
then consider x being Function of S,(TopSpaceMetr T) such that
A8: ( a = x & x is continuous ) ;
b in ContinuousFunctions (S,T) ;
then consider y being Function of S,(TopSpaceMetr T) such that
A9: ( b = y & y is continuous ) ;
consider Dist being RealMap of S such that
A10: ( ( for t being Point of S holds Dist . t = dist ((In ((x . t),T)),(In ((y . t),T))) ) & f . (a,b) = upper_bound (rng Dist) ) by Def5, A8, A9;
A11: ( rng Dist <> {} & rng Dist is bounded_above & rng Dist is bounded_below ) by A8, A9, A10, Th9;

now :: thesis: for t being Point of S holds x . t = y . t

let t be Point of S; :: thesis: x . t = y . t
A12: Dist . t = dist ((In ((x . t),T)),(In ((y . t),T))) by A10;
A13: 0 <= dist ((In ((x . t),T)),(In ((y . t),T))) by METRIC_1:5;
dist ((In ((x . t),T)),(In ((y . t),T))) in rng Dist by FUNCT_2:112, A12;
then dist ((In ((x . t),T)),(In ((y . t),T))) = 0 by A13, A7, A10, SEQ_4:def 1, A11;
hence x . t = y . t by METRIC_1:2; :: thesis: verum

end;

hence a = b by A8, A9, FUNCT_2:63; :: thesis: verum

end;

then A14: f is discerning ;
for a, b being Element of ContinuousFunctions (S,T) holds f . (a,b) = f . (b,a)

proof

let a, b be Element of ContinuousFunctions (S,T); :: thesis: f . (a,b) = f . (b,a)
a in ContinuousFunctions (S,T) ;
then consider x being Function of S,(TopSpaceMetr T) such that
A15: ( a = x & x is continuous ) ;
b in ContinuousFunctions (S,T) ;
then consider y being Function of S,(TopSpaceMetr T) such that
A16: ( b = y & y is continuous ) ;
consider Dist1 being RealMap of S such that
A17: ( ( 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, A15, A16;
consider Dist2 being RealMap of S such that
A18: ( ( for t being Point of S holds Dist2 . t = dist ((In ((y . t),T)),(In ((x . t),T))) ) & f . (b,a) = upper_bound (rng Dist2) ) by Def5, A15, A16;
for t being Point of S holds Dist1 . t = Dist2 . t

proof

let t be Point of S; :: thesis: Dist1 . t = Dist2 . t
thus Dist1 . t = dist ((In ((x . t),T)),(In ((y . t),T))) by A17
.= dist ((In ((y . t),T)),(In ((x . t),T)))
.= Dist2 . t by A18 ; :: thesis: verum

end;

hence f . (a,b) = f . (b,a) by A17, A18, FUNCT_2:63; :: thesis: verum

end;

then A19: f is symmetric ;
for a, b, c being Element of ContinuousFunctions (S,T) holds f . (a,c) <= (f . (a,b)) + (f . (b,c))

proof

let a, b, c be Element of ContinuousFunctions (S,T); :: thesis: f . (a,c) <= (f . (a,b)) + (f . (b,c))
a in ContinuousFunctions (S,T) ;
then consider x being Function of S,(TopSpaceMetr T) such that
A20: ( a = x & x is continuous ) ;
b in ContinuousFunctions (S,T) ;
then consider y being Function of S,(TopSpaceMetr T) such that
A21: ( b = y & y is continuous ) ;
c in ContinuousFunctions (S,T) ;
then consider z being Function of S,(TopSpaceMetr T) such that
A22: ( c = z & z is continuous ) ;
consider Dist1 being RealMap of S such that
A23: ( ( 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, A20, A21;
consider Dist2 being RealMap of S such that
A24: ( ( for t being Point of S holds Dist2 . t = dist ((In ((y . t),T)),(In ((z . t),T))) ) & f . (b,c) = upper_bound (rng Dist2) ) by Def5, A21, A22;
consider Dist3 being RealMap of S such that
A25: ( ( for t being Point of S holds Dist3 . t = dist ((In ((x . t),T)),(In ((z . t),T))) ) & f . (a,c) = upper_bound (rng Dist3) ) by Def5, A20, A22;
A26: ( rng Dist1 <> {} & rng Dist1 is bounded_above & rng Dist1 is bounded_below ) by A20, A21, A23, Th9;
A27: ( rng Dist2 <> {} & rng Dist2 is bounded_above & rng Dist2 is bounded_below ) by A21, A22, A24, Th9;
A28: ( rng Dist3 <> {} & rng Dist3 is bounded_above & rng Dist3 is bounded_below ) by A20, A22, A25, Th9;

now :: thesis: for r being Real st r in rng Dist3 holds
r <= (f . (a,b)) + (f . (b,c))

let r be Real; :: thesis: ( r in rng Dist3 implies r <= (f . (a,b)) + (f . (b,c)) )
assume r in rng Dist3 ; :: thesis: r <= (f . (a,b)) + (f . (b,c))
then consider t being Element of S such that
A29: r = Dist3 . t by FUNCT_2:113;
A30: Dist3 . t = dist ((In ((x . t),T)),(In ((z . t),T))) by A25;
A31: Dist1 . t = dist ((In ((x . t),T)),(In ((y . t),T))) by A23;
Dist2 . t = dist ((In ((y . t),T)),(In ((z . t),T))) by A24;
then A33: Dist3 . t <= (Dist1 . t) + (Dist2 . t) by A30, A31, METRIC_1:4;
Dist1 . t in rng Dist1 by FUNCT_2:112;
then A34: Dist1 . t <= f . (a,b) by A26, A23, SEQ_4:def 1;
Dist2 . t in rng Dist2 by FUNCT_2:112;
then Dist2 . t <= f . (b,c) by A27, A24, SEQ_4:def 1;
then (Dist1 . t) + (Dist2 . t) <= (f . (a,b)) + (f . (b,c)) by A34, XREAL_1:7;
hence r <= (f . (a,b)) + (f . (b,c)) by A29, A33, XXREAL_0:2; :: thesis: verum

end;

hence f . (a,c) <= (f . (a,b)) + (f . (b,c)) by A28, SEQ_4:45, A25; :: thesis: verum

end;

then f is triangle ;
hence ( MetricSpace_of_ContinuousFunctions (S,T) is Reflexive & MetricSpace_of_ContinuousFunctions (S,T) is discerning & MetricSpace_of_ContinuousFunctions (S,T) is symmetric & MetricSpace_of_ContinuousFunctions (S,T) is triangle ) by A6, A14, A19; :: thesis: verum