let T be non empty TopSpace; :: thesis: for f being RealMap of T st f is continuous holds
for F being RealMap of [:T,T:] st ( for x, y being Element of T holds F . (x,y) = |.((f . x) - (f . y)).| ) holds
F is continuous
let f be RealMap of T; :: thesis: ( f is continuous implies for F being RealMap of [:T,T:] st ( for x, y being Element of T holds F . (x,y) = |.((f . x) - (f . y)).| ) holds
F is continuous )
assume A1: f is continuous ; :: thesis: for F being RealMap of [:T,T:] st ( for x, y being Element of T holds F . (x,y) = |.((f . x) - (f . y)).| ) holds
F is continuous
set TT = [:T,T:];
set cT = the carrier of T;
reconsider f9 = f as Function of T,R^1 by TOPMETR:17;
let F be RealMap of [:T,T:]; :: thesis: ( ( for x, y being Element of T holds F . (x,y) = |.((f . x) - (f . y)).| ) implies F is continuous )
assume A2: for x, y being Element of T holds F . (x,y) = |.((f . x) - (f . y)).| ; :: thesis: F is continuous
reconsider F9 = F as Function of [:T,T:],R^1 by TOPMETR:17;
A3: f9 is continuous by A1, JORDAN5A:27;

now :: thesis: for tt being Point of [:T,T:] holds F9 is_continuous_at tt

let tt be Point of [:T,T:]; :: thesis: F9 is_continuous_at tt
tt in the carrier of [:T,T:] ;
then tt in [: the carrier of T, the carrier of T:] by BORSUK_1:def 2;
then consider t1, t2 being object such that
A4: ( t1 in the carrier of T & t2 in the carrier of T ) and
A5: [t1,t2] = tt by ZFMISC_1:def 2;
reconsider t1 = t1, t2 = t2 as Point of T by A4;
for R being Subset of R^1 st R is open & F9 . tt in R holds
ex H being Subset of [:T,T:] st
( H is open & tt in H & F9 .: H c= R )

proof

reconsider ft1 = f . t1, ft2 = f . t2 as Point of RealSpace by METRIC_1:def 13;
reconsider Ftt = F . tt as Point of RealSpace by METRIC_1:def 13;
let R be Subset of R^1; :: thesis: ( R is open & F9 . tt in R implies ex H being Subset of [:T,T:] st
( H is open & tt in H & F9 .: H c= R ) )
assume ( R is open & F9 . tt in R ) ; :: thesis: ex H being Subset of [:T,T:] st
( H is open & tt in H & F9 .: H c= R )
then consider r being Real such that
A6: r > 0 and
A7: Ball (Ftt,r) c= R by TOPMETR:15, TOPMETR:def 6;
reconsider r9 = r as Real ;
reconsider A = Ball (ft1,(r9 / 2)), B = Ball (ft2,(r9 / 2)) as Subset of R^1 by METRIC_1:def 13, TOPMETR:17;
A8: ( A is open & f9 is_continuous_at t1 ) by A3, TMAP_1:50, TOPMETR:14, TOPMETR:def 6;
f . t1 in A by A6, Lm7, XREAL_1:139;
then consider T1 being Subset of T such that
A9: T1 is open and
A10: t1 in T1 and
A11: f9 .: T1 c= A by A8, TMAP_1:43;
A12: ( B is open & f9 is_continuous_at t2 ) by A3, TMAP_1:50, TOPMETR:14, TOPMETR:def 6;
f . t2 in B by A6, Lm7, XREAL_1:139;
then consider T2 being Subset of T such that
A13: T2 is open and
A14: t2 in T2 and
A15: f9 .: T2 c= B by A12, TMAP_1:43;
F . tt = F . (t1,t2) by A5;
then A16: |.((f9 . t1) - (f9 . t2)).| = F . tt by A2;
A17: F .: [:T1,T2:] c= R

proof

let Fxy be object ; :: according to TARSKI:def 3 :: thesis: ( not Fxy in F .: [:T1,T2:] or Fxy in R )
assume Fxy in F .: [:T1,T2:] ; :: thesis: Fxy in R
then consider xy being object such that
xy in dom F and
A18: xy in [:T1,T2:] and
A19: Fxy = F . xy by FUNCT_1:def 6;
consider x, y being object such that
A20: x in T1 and
A21: y in T2 and
A22: xy = [x,y] by A18, ZFMISC_1:def 2;
reconsider x = x, y = y as Point of T by A20, A21;
reconsider fx = f . x, fy = f . y as Point of RealSpace by METRIC_1:def 13;
y in the carrier of T ;
then y in dom f by FUNCT_2:def 1;
then f . y in f .: T2 by A21, FUNCT_1:def 6;
then A23: dist (fy,ft2) < r9 / 2 by A15, METRIC_1:11;
reconsider Fxy1 = F . [x,y] as Point of RealSpace by METRIC_1:def 13;
A24: |.((f . x) - (f . y)).| = F . (x,y) by A2;
then F . [x,y] <= (|.((f . x) - (f . t1)).| + (F . tt)) + |.((f . t2) - (f . y)).| by A16, Lm2;
then F . [x,y] <= (|.((f . x) - (f . t1)).| + (F . tt)) + (dist (ft2,fy)) by TOPMETR:11;
then A25: (F . [x,y]) + 0 <= ((F . tt) + (dist (fx,ft1))) + (dist (ft2,fy)) by TOPMETR:11;
F . tt <= (|.((f . t1) - (f . x)).| + (F . [x,y])) + |.((f . y) - (f . t2)).| by A16, A24, Lm2;
then F . tt <= ((dist (fx,ft1)) + (F . [x,y])) + |.((f . y) - (f . t2)).| by TOPMETR:11;
then A26: F . tt <= ((F . [x,y]) + (dist (fx,ft1))) + (dist (fy,ft2)) by TOPMETR:11;
x in the carrier of T ;
then x in dom f by FUNCT_2:def 1;
then f . x in f .: T1 by A20, FUNCT_1:def 6;
then dist (fx,ft1) < r9 / 2 by A11, METRIC_1:11;
then A27: (dist (fx,ft1)) + (dist (fy,ft2)) < (r9 / 2) + (r9 / 2) by A23, XREAL_1:8;
then (F . [x,y]) + ((dist (fx,ft1)) + (dist (fy,ft2))) < (F . [x,y]) + r9 by XREAL_1:8;
then F . tt < - ((- (F . [x,y])) - r9) by A26, XXREAL_0:2;
then (- (F . tt)) - 0 > (- r9) - (F . [x,y]) by XREAL_1:26;
then A28: (- (F . tt)) + (F . [x,y]) > (- r9) + 0 by XREAL_1:21;
(F . tt) + ((dist (fx,ft1)) + (dist (ft2,fy))) < (F . tt) + r9 by A27, XREAL_1:8;
then (F . [x,y]) + 0 < (F . tt) + r9 by A25, XXREAL_0:2;
then (F . [x,y]) - (F . tt) < r9 - 0 by XREAL_1:21;
then |.((F . [x,y]) - (F . tt)).| < r9 by A28, SEQ_2:1;
then dist (Ftt,Fxy1) < r9 by TOPMETR:11;
then Fxy1 in Ball (Ftt,r) by METRIC_1:11;
hence Fxy in R by A7, A19, A22; :: thesis: verum

end;

tt in [:T1,T2:] by A5, A10, A14, ZFMISC_1:def 2;
hence ex H being Subset of [:T,T:] st
( H is open & tt in H & F9 .: H c= R ) by A9, A13, A17, BORSUK_1:6; :: thesis: verum

end;

hence F9 is_continuous_at tt by TMAP_1:43; :: thesis: verum

end;

then F9 is continuous by TMAP_1:50;
hence F is continuous by JORDAN5A:27; :: thesis: verum