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;

hence F is continuous by JORDAN5A:27; :: thesis: verum

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

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

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

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

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

tt in [:T1,T2:]
by A5, A10, A14, ZFMISC_1:def 2;
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;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

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

hence F is continuous by JORDAN5A:27; :: thesis: verum