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 A2, Def2, TMAP_1:50;
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 A4, TMAP_1:43;
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 A6, XBOOLE_0:def 4;
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 A3, FUNCT_1:def 6;
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 A11, FUNCT_1:def 6;
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 A13, ZFMISC_1:def 2;
reconsider x9 = x9, u9 = u9 as Point of T by A16;
[x9,u9] in [:{x}, the carrier of T:] by A14, A17, XBOOLE_0:def 4;
then ( (pr2 ( the carrier of T, the carrier of T)) . (x9,u9) = u9 & x9 = x ) by FUNCT_3:def 5, ZFMISC_1:105;
then A18: pmet . (x9,u9) = du by A12, A15, A17, Def2;
A19: dom pmetR = the carrier of [:T,T:] by FUNCT_2:def 1;
[x9,u9] in XU by A14, A17, XBOOLE_0:def 4;
then du in pmetR .: XU by A18, A19, FUNCT_1:def 6;
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 A5, Th3;
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