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;

hence dist (pmet,x) is continuous by JORDAN5A:27; :: thesis: verum

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

then
distx is continuous
by TMAP_1:50;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 )

end;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

hence
distx is_continuous_at t
by TMAP_1:43; :: thesis: verum
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

hence ex U being Subset of T st

( U is open & t in U & distx .: U c= R ) by A8, A9; :: thesis: verum

end;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

(pr2 ( the carrier of T, the carrier of T)) .: (XU /\ [:{x}, the carrier of T:]) is open
by A5, Th3;
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;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

hence ex U being Subset of T st

( U is open & t in U & distx .: U c= R ) by A8, A9; :: thesis: verum

hence dist (pmet,x) is continuous by JORDAN5A:27; :: thesis: verum