let T be non empty TopSpace; :: thesis: for pmet being Function of [:the carrier of T,the carrier of T:],REAL st ( for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' 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 pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) implies for x being Point of T holds dist pmet,x is continuous )
assume A1: for pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ; :: thesis: for x being Point of T holds dist pmet,x is continuous
let x be Point of T; :: thesis: dist pmet,x is continuous
[:the carrier of T,the carrier of T:] = the carrier of [:T,T:] by BORSUK_1:def 5;
then reconsider pmet' = pmet as RealMap of [:T,T:] ;
reconsider pmetR = pmet' as Function of [:T,T:],R^1 by TOPMETR:24;
reconsider distx = dist pmet,x as Function of T,R^1 by TOPMETR:24;
pmet' is continuous by A1;
then A2: pmetR is continuous by TOPREAL6:83;

now

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

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 A3: ( 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 )
reconsider xt = [x,t] as Point of [:T,T:] by BORSUK_1:def 5;
( pmetR is_continuous_at xt & distx . t = pmet . x,t & pmet . x,t = pmet . xt ) by A2, Def2, TMAP_1:55;
then consider XU being Subset of [:T,T:] such that
A4: ( XU is open & xt in XU & pmetR .: XU c= R ) by A3, TMAP_1:48;
set U = (pr2 the carrier of T,the carrier of T) .: (XU /\ [:{x},the carrier of T:]);
( [x,t] in XU & [x,t] in [:{x},the carrier of T:] ) by A4, ZFMISC_1:128;
then ( [x,t] in XU /\ [:{x},the carrier of T:] & dom (pr2 the carrier of T,the carrier of T) = [:the carrier of T,the carrier of T:] & [x,t] in [:the carrier of T,the carrier of T:] ) by FUNCT_3:def 6, 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 FUNCT_1:def 12;
then A5: ( t in (pr2 the carrier of T,the carrier of T) .: (XU /\ [:{x},the carrier of T:]) & (pr2 the carrier of T,the carrier of T) .: (XU /\ [:{x},the carrier of T:]) is open ) by A4, Th3, FUNCT_3:def 6;
distx .: ((pr2 the carrier of T,the carrier of T) .: (XU /\ [:{x},the carrier of T:])) c= R

proof

let du be set ; :: 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 A6: du in distx .: ((pr2 the carrier of T,the carrier of T) .: (XU /\ [:{x},the carrier of T:])) ; :: thesis: du in R
consider u being set such that
A7: ( u in dom distx & u in (pr2 the carrier of T,the carrier of T) .: (XU /\ [:{x},the carrier of T:]) & distx . u = du ) by A6, FUNCT_1:def 12;
reconsider u = u as Point of T by A7;
consider xu being set such that
A8: ( xu in dom (pr2 the carrier of T,the carrier of T) & xu in XU /\ [:{x},the carrier of T:] & (pr2 the carrier of T,the carrier of T) . xu = u ) by A7, FUNCT_1:def 12;
consider x', u' being set such that
A9: ( x' in the carrier of T & u' in the carrier of T & xu = [x',u'] ) by A8, ZFMISC_1:def 2;
reconsider x' = x', u' = u' as Point of T by A9;
( [x',u'] in [:{x},the carrier of T:] & (pr2 the carrier of T,the carrier of T) . x',u' = u' ) by A8, A9, FUNCT_3:def 6, XBOOLE_0:def 4;
then ( x' = x & u' = u ) by A8, A9, ZFMISC_1:128;
then ( pmet . x',u' = du & [x',u'] in XU & pmet' . [x',u'] = pmet . x',u' & dom pmetR = the carrier of [:T,T:] ) by A7, A8, A9, Def2, FUNCT_2:def 1, XBOOLE_0:def 4;
then du in pmetR .: XU by FUNCT_1:def 12;
hence du in R by A4; :: thesis: verum

end;

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

end;

hence distx is_continuous_at t by TMAP_1:48; :: thesis: verum

end;

then distx is continuous by TMAP_1:55;
hence dist pmet,x is continuous by TOPREAL6:83; :: thesis: verum