let F1, F2 be Function of [:(ContinuousFunctions (S,T)),(ContinuousFunctions (S,T)):],REAL; :: thesis: ( ( for f, g being Function of S,(TopSpaceMetr T) st f in ContinuousFunctions (S,T) & g in ContinuousFunctions (S,T) holds
ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & F1 . (f,g) = upper_bound (rng Dist) ) ) & ( for f, g being Function of S,(TopSpaceMetr T) st f in ContinuousFunctions (S,T) & g in ContinuousFunctions (S,T) holds
ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & F2 . (f,g) = upper_bound (rng Dist) ) ) implies F1 = F2 )
assume that
A1: for f, g being Function of S,(TopSpaceMetr T) st f in ContinuousFunctions (S,T) & g in ContinuousFunctions (S,T) holds
ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & F1 . (f,g) = upper_bound (rng Dist) ) and
A2: for f, g being Function of S,(TopSpaceMetr T) st f in ContinuousFunctions (S,T) & g in ContinuousFunctions (S,T) holds
ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & F2 . (f,g) = upper_bound (rng Dist) ) ; :: thesis: F1 = F2
set H = ContinuousFunctions (S,T);
for x, y being set st x in ContinuousFunctions (S,T) & y in ContinuousFunctions (S,T) holds
F1 . (x,y) = F2 . (x,y)

proof

let x, y be set ; :: thesis: ( x in ContinuousFunctions (S,T) & y in ContinuousFunctions (S,T) implies F1 . (x,y) = F2 . (x,y) )
assume A3: ( x in ContinuousFunctions (S,T) & y in ContinuousFunctions (S,T) ) ; :: thesis: F1 . (x,y) = F2 . (x,y)
then consider f being Function of S,(TopSpaceMetr T) such that
A4: ( x = f & f is continuous ) ;
consider g being Function of S,(TopSpaceMetr T) such that
A5: ( y = g & g is continuous ) by A3;
consider Dist1 being RealMap of S such that
A6: ( ( for x being Point of S holds Dist1 . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & F1 . (f,g) = upper_bound (rng Dist1) ) by A1, A3, A4, A5;
consider Dist2 being RealMap of S such that
A7: ( ( for x being Point of S holds Dist2 . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & F2 . (f,g) = upper_bound (rng Dist2) ) by A2, A3, A4, A5;
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 ((f . t),T)),(In ((g . t),T))) by A6
.= Dist2 . t by A7 ; :: thesis: verum

end;

hence F1 . (x,y) = F2 . (x,y) by A4, A5, A6, A7, FUNCT_2:63; :: thesis: verum

end;

hence F1 = F2 by BINOP_1:1; :: thesis: verum