let S be non empty 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
Dist is continuous
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
Dist is continuous
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
Dist is continuous )
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
Dist is continuous
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 Dist is continuous )
assume A3: for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ; :: thesis: Dist is continuous

now :: thesis: for x being Point of S
for V being Subset of REAL st Dist . x in V & V is open holds
ex W being Element of bool the carrier of S st
( x in W & W is open & Dist .: W c= V )

let x be Point of S; :: thesis: for V being Subset of REAL st Dist . x in V & V is open holds
ex W being Element of bool the carrier of S st
( x in W & W is open & Dist .: W c= V )
let V be Subset of REAL; :: thesis: ( Dist . x in V & V is open implies ex W being Element of bool the carrier of S st
( x in W & W is open & Dist .: W c= V ) )
assume ( Dist . x in V & V is open ) ; :: thesis: ex W being Element of bool the carrier of S st
( x in W & W is open & Dist .: W c= V )
then consider e being Real such that
A5: ( 0 < e & ].((Dist . x) - e),((Dist . x) + e).[ c= V ) by RCOMP_1:19;
f is_continuous_at x by A1, TMAP_1:50;
then consider F being Subset of S such that
A6: ( F is open & x in F & ( for y being Point of S st y in F holds
dist ((In ((f . x),T)),(In ((f . y),T))) < e / 2 ) ) by Th2, A5;
consider G being Subset of S such that
A7: ( G is open & x in G & ( for y being Point of S st y in G holds
dist ((In ((g . x),T)),(In ((g . y),T))) < e / 2 ) ) by Th2, A5, A2, TMAP_1:50;
take W = F /\ G; :: thesis: ( x in W & W is open & Dist .: W c= V )
thus x in W by A6, A7, XBOOLE_0:def 4; :: thesis: ( W is open & Dist .: W c= V )
thus W is open by A6, A7; :: thesis: Dist .: W c= V
thus Dist .: W c= V :: thesis: verum

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Dist .: W or z in V )
assume z in Dist .: W ; :: thesis: z in V
then consider t being object such that
A8: ( t in dom Dist & t in W & z = Dist . t ) by FUNCT_1:def 6;
reconsider t = t as Point of S by A8;
t in F by A8, XBOOLE_0:def 4;
then A9: dist ((In ((f . x),T)),(In ((f . t),T))) < e / 2 by A6;
t in G by A8, XBOOLE_0:def 4;
then A10: dist ((In ((g . x),T)),(In ((g . t),T))) < e / 2 by A7;
A11: z = dist ((In ((f . t),T)),(In ((g . t),T))) by A8, A3;
(dist ((In ((f . t),T)),(In ((g . t),T)))) - (Dist . x) = (dist ((In ((f . t),T)),(In ((g . t),T)))) - (dist ((In ((f . x),T)),(In ((g . x),T)))) by A3;
then A13: |.((dist ((In ((f . t),T)),(In ((g . t),T)))) - (Dist . x)).| <= (dist ((In ((f . t),T)),(In ((f . x),T)))) + (dist ((In ((g . t),T)),(In ((g . x),T)))) by Th7;
(dist ((In ((f . t),T)),(In ((f . x),T)))) + (dist ((In ((g . t),T)),(In ((g . x),T)))) < (e / 2) + (e / 2) by A9, A10, XREAL_1:8;
then |.((dist ((In ((f . t),T)),(In ((g . t),T)))) - (Dist . x)).| < e by A13, XXREAL_0:2;
hence z in V by A5, A11, RCOMP_1:1; :: thesis: verum

end;

end;

hence Dist is continuous by C0SP2:1; :: thesis: verum