let S be non empty compact TopSpace; :: thesis: for T being non empty MetrSpace
for f, g being Function of S,(TopSpaceMetr T) st f is continuous & g is continuous holds
for Dist being RealMap of S st ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) holds
( rng Dist <> {} & rng Dist is bounded_above & rng Dist is bounded_below )
let T be non empty MetrSpace; :: thesis: for f, g being Function of S,(TopSpaceMetr T) st f is continuous & g is continuous holds
for Dist being RealMap of S st ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) holds
( rng Dist <> {} & rng Dist is bounded_above & rng Dist is bounded_below )
let f, g be Function of S,(TopSpaceMetr T); :: thesis: ( f is continuous & g is continuous implies for Dist being RealMap of S st ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) holds
( rng Dist <> {} & rng Dist is bounded_above & rng Dist is bounded_below ) )
assume that
A1: f is continuous and
A2: g is continuous ; :: thesis: for Dist being RealMap of S st ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) holds
( rng Dist <> {} & rng Dist is bounded_above & rng Dist is bounded_below )
let Dist be RealMap of S; :: thesis: ( ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) implies ( rng Dist <> {} & rng Dist is bounded_above & rng Dist is bounded_below ) )
assume A3: for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ; :: thesis: ( rng Dist <> {} & rng Dist is bounded_above & rng Dist is bounded_below )
S is pseudocompact ;
then Dist is bounded by A1, A2, A3, Th8;
then A5: ( Dist is bounded_above & Dist is bounded_below ) ;
thus rng Dist <> {} by FUNCT_2:112; :: thesis: ( rng Dist is bounded_above & rng Dist is bounded_below )
consider K being Real such that
A6: for t being object st t in dom Dist holds
Dist . t < K by A5;

now :: thesis: for r being ExtReal st r in rng Dist holds
r <= K

let r be ExtReal; :: thesis: ( r in rng Dist implies r <= K )
assume r in rng Dist ; :: thesis: r <= K
then consider t being Element of S such that
A7: r = Dist . t by FUNCT_2:113;
dom Dist = the carrier of S by FUNCT_2:def 1;
hence r <= K by A6, A7; :: thesis: verum

end;

then K is UpperBound of rng Dist by XXREAL_2:def 1;
hence rng Dist is bounded_above ; :: thesis: rng Dist is bounded_below
consider K being Real such that
A8: for t being object st t in dom Dist holds
K < Dist . t by A5;

now :: thesis: for r being ExtReal st r in rng Dist holds
K <= r

let r be ExtReal; :: thesis: ( r in rng Dist implies K <= r )
assume r in rng Dist ; :: thesis: K <= r
then consider t being Element of S such that
A9: r = Dist . t by FUNCT_2:113;
dom Dist = the carrier of S by FUNCT_2:def 1;
hence K <= r by A8, A9; :: thesis: verum

end;

then K is LowerBound of rng Dist by XXREAL_2:def 2;
hence rng Dist is bounded_below ; :: thesis: verum