let T be non empty TopSpace; :: thesis: for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) holds
for x being Point of T holds dist (pmet,x) is continuous

set cT = the carrier of T;
let pmet be Function of [: the carrier of T, the carrier of T:],REAL; :: thesis: ( ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) implies for x being Point of T holds dist (pmet,x) is continuous )

assume A1: for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ; :: thesis: for x being Point of T holds dist (pmet,x) is continuous
[: the carrier of T, the carrier of T:] = the carrier of [:T,T:] by BORSUK_1:def 2;
then reconsider pmet9 = pmet as RealMap of [:T,T:] ;
reconsider pmetR = pmet9 as Function of [:T,T:],R^1 by TOPMETR:17;
let x be Point of T; :: thesis: dist (pmet,x) is continuous
reconsider distx = dist (pmet,x) as Function of T,R^1 by TOPMETR:17;
pmet9 is continuous by A1;
then A2: pmetR is continuous by JORDAN5A:27;
now :: thesis: for t being Point of T holds distx is_continuous_at t
let t be Point of T; :: thesis: distx is_continuous_at t
for R being Subset of R^1 st R is open & distx . t in R holds
ex U being Subset of T st
( U is open & t in U & distx .: U c= R )
proof
reconsider xt = [x,t] as Point of [:T,T:] by BORSUK_1:def 2;
A3: dom (pr2 ( the carrier of T, the carrier of T)) = [: the carrier of T, the carrier of T:] by FUNCT_3:def 5;
A4: ( pmetR is_continuous_at xt & distx . t = pmet . (x,t) ) by ;
let R be Subset of R^1; :: thesis: ( R is open & distx . t in R implies ex U being Subset of T st
( U is open & t in U & distx .: U c= R ) )

assume ( R is open & distx . t in R ) ; :: thesis: ex U being Subset of T st
( U is open & t in U & distx .: U c= R )

then consider XU being Subset of [:T,T:] such that
A5: XU is open and
A6: xt in XU and
A7: pmetR .: XU c= R by ;
set U = (pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]);
[x,t] in [:{x}, the carrier of T:] by ZFMISC_1:105;
then [x,t] in XU /\ [:{x}, the carrier of T:] by ;
then (pr2 ( the carrier of T, the carrier of T)) . (x,t) in (pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]) by ;
then A8: t in (pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]) by FUNCT_3:def 5;
A9: distx .: ((pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:])) c= R
proof
let du be object ; :: according to TARSKI:def 3 :: thesis: ( not du in distx .: ((pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:])) or du in R )
assume du in distx .: ((pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:])) ; :: thesis: du in R
then consider u being object such that
A10: u in dom distx and
A11: u in (pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]) and
A12: distx . u = du by FUNCT_1:def 6;
reconsider u = u as Point of T by A10;
consider xu being object such that
A13: xu in dom (pr2 ( the carrier of T, the carrier of T)) and
A14: xu in XU /\ [:{x}, the carrier of T:] and
A15: (pr2 ( the carrier of T, the carrier of T)) . xu = u by ;
consider x9, u9 being object such that
A16: ( x9 in the carrier of T & u9 in the carrier of T ) and
A17: xu = [x9,u9] by ;
reconsider x9 = x9, u9 = u9 as Point of T by A16;
[x9,u9] in [:{x}, the carrier of T:] by ;
then ( (pr2 ( the carrier of T, the carrier of T)) . (x9,u9) = u9 & x9 = x ) by ;
then A18: pmet . (x9,u9) = du by ;
A19: dom pmetR = the carrier of [:T,T:] by FUNCT_2:def 1;
[x9,u9] in XU by ;
then du in pmetR .: XU by ;
hence du in R by A7; :: thesis: verum
end;
(pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]) is open by ;
hence ex U being Subset of T st
( U is open & t in U & distx .: U c= R ) by A8, A9; :: thesis: verum
end;
hence distx is_continuous_at t by TMAP_1:43; :: thesis: verum
end;
then distx is continuous by TMAP_1:50;
hence dist (pmet,x) is continuous by JORDAN5A:27; :: thesis: verum