let S be non empty TopSpace; :: thesis: for T being non empty MetrSpace ex F being Function of [:(ContinuousFunctions (S,T)),(ContinuousFunctions (S,T)):],REAL st
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))) ) & F . (f,g) = upper_bound (rng Dist) )
let T be non empty MetrSpace; :: thesis: ex F being Function of [:(ContinuousFunctions (S,T)),(ContinuousFunctions (S,T)):],REAL st
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))) ) & F . (f,g) = upper_bound (rng Dist) )
set F1 = ContinuousFunctions (S,T);
defpred S₁[ object , object , object ] means ex f, g being Function of S,(TopSpaceMetr T) ex Dist being RealMap of S st
( $1 = f & $2 = g & ( for t being Point of S holds Dist . t = dist ((In ((f . t),T)),(In ((g . t),T))) ) & $3 = upper_bound (rng Dist) );
A1: for x, y being object st x in ContinuousFunctions (S,T) & y in ContinuousFunctions (S,T) holds
ex z being object st
( z in REAL & S₁[x,y,z] )

proof

let x, y be object ; :: thesis: ( x in ContinuousFunctions (S,T) & y in ContinuousFunctions (S,T) implies ex z being object st
( z in REAL & S₁[x,y,z] ) )
assume A2: ( x in ContinuousFunctions (S,T) & y in ContinuousFunctions (S,T) ) ; :: thesis: ex z being object st
( z in REAL & S₁[x,y,z] )
then consider f being Function of S,(TopSpaceMetr T) such that
A3: ( x = f & f is continuous ) ;
consider g being Function of S,(TopSpaceMetr T) such that
A4: ( y = g & g is continuous ) by A2;
deffunc H₁( object ) -> object = dist ((In ((f . $1),T)),(In ((g . $1),T)));
A5: for t being object st t in the carrier of S holds
H₁(t) in REAL by XREAL_0:def 1;
consider Dist being Function of the carrier of S,REAL such that
A6: for t being object st t in the carrier of S holds
Dist . t = H₁(t) from FUNCT_2:sch 2(A5);
reconsider Dist = Dist as RealMap of S ;
A7: for t being Point of S holds Dist . t = dist ((In ((f . t),T)),(In ((g . t),T))) by A6;
take z = upper_bound (rng Dist); :: thesis: ( z in REAL & S₁[x,y,z] )
thus z in REAL by XREAL_0:def 1; :: thesis: S₁[x,y,z]
thus S₁[x,y,z] by A3, A4, A7; :: thesis: verum

end;

consider F being Function of [:(ContinuousFunctions (S,T)),(ContinuousFunctions (S,T)):],REAL such that
A8: for x, y being object st x in ContinuousFunctions (S,T) & y in ContinuousFunctions (S,T) holds
S₁[x,y,F . (x,y)] from BINOP_1:sch 1(A1);
take F ; :: 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))) ) & F . (f,g) = upper_bound (rng Dist) )
let f1, g1 be Function of S,(TopSpaceMetr T); :: thesis: ( f1 in ContinuousFunctions (S,T) & g1 in ContinuousFunctions (S,T) implies ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f1 . x),T)),(In ((g1 . x),T))) ) & F . (f1,g1) = upper_bound (rng Dist) ) )
assume ( f1 in ContinuousFunctions (S,T) & g1 in ContinuousFunctions (S,T) ) ; :: thesis: ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f1 . x),T)),(In ((g1 . x),T))) ) & F . (f1,g1) = upper_bound (rng Dist) )
then ex f, g being Function of S,(TopSpaceMetr T) ex Dist being RealMap of S st
( f1 = f & g1 = g & ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & F . (f1,g1) = upper_bound (rng Dist) ) by A8;
hence ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f1 . x),T)),(In ((g1 . x),T))) ) & F . (f1,g1) = upper_bound (rng Dist) ) ; :: thesis: verum