let f be PartFunc of REAL,REAL; :: thesis: for Y being Subset of REAL st Y c= dom f & Y is compact & f | Y is continuous holds

f | Y is uniformly_continuous

let Y be Subset of REAL; :: thesis: ( Y c= dom f & Y is compact & f | Y is continuous implies f | Y is uniformly_continuous )

assume that

A1: Y c= dom f and

A2: Y is compact and

A3: f | Y is continuous ; :: thesis: f | Y is uniformly_continuous

assume not f | Y is uniformly_continuous ; :: thesis: contradiction

then consider r being Real such that

A4: 0 < r and

A5: for s being Real st 0 < s holds

ex x1, x2 being Real st

( x1 in dom (f | Y) & x2 in dom (f | Y) & |.(x1 - x2).| < s & not |.((f . x1) - (f . x2)).| < r ) by Th1;

defpred S_{1}[ Element of NAT , Real] means ( $2 in Y & ex x2 being Element of REAL st

( x2 in Y & |.($2 - x2).| < 1 / ($1 + 1) & not |.((f . $2) - (f . x2)).| < r ) );

A8: for n being Element of NAT holds S_{1}[n,s1 . n]
from FUNCT_2:sch 3(A6);

then consider q1 being Real_Sequence such that

A10: q1 is subsequence of s1 and

A11: q1 is convergent and

A12: lim q1 in Y by A2, RCOMP_1:def 3;

lim q1 in dom (f | Y) by A1, A12, RELAT_1:57;

then A13: f | Y is_continuous_in lim q1 by A3, FCONT_1:def 2;

rng q1 c= rng s1 by A10, VALUED_0:21;

then A14: rng q1 c= Y by A9, XBOOLE_1:1;

then rng q1 c= dom f by A1, XBOOLE_1:1;

then rng q1 c= (dom f) /\ Y by A14, XBOOLE_1:19;

then A15: rng q1 c= dom (f | Y) by RELAT_1:61;

then A16: (f | Y) . (lim q1) = lim ((f | Y) /* q1) by A11, A13, FCONT_1:def 1;

A17: (f | Y) /* q1 is convergent by A11, A13, A15, FCONT_1:def 1;

defpred S_{2}[ Element of NAT , Real] means ( $2 in Y & |.((s1 . $1) - $2).| < 1 / ($1 + 1) & not |.((f . (s1 . $1)) - (f . $2)).| < r );

A18: for n being Element of NAT ex x2 being Element of REAL st S_{2}[n,x2]
by A8;

consider s2 being Real_Sequence such that

A19: for n being Element of NAT holds S_{2}[n,s2 . n]
from FUNCT_2:sch 3(A18);

consider Ns1 being V46() sequence of NAT such that

A21: q1 = s1 * Ns1 by A10, VALUED_0:def 17;

set q2 = q1 - ((s1 - s2) * Ns1);

q1 - ((s1 - s2) * Ns1) is subsequence of s2 by A22, FUNCT_2:63, VALUED_0:def 17;

then rng (q1 - ((s1 - s2) * Ns1)) c= rng s2 by VALUED_0:21;

then A24: rng (q1 - ((s1 - s2) * Ns1)) c= Y by A20, XBOOLE_1:1;

then rng (q1 - ((s1 - s2) * Ns1)) c= dom f by A1, XBOOLE_1:1;

then rng (q1 - ((s1 - s2) * Ns1)) c= (dom f) /\ Y by A24, XBOOLE_1:19;

then A25: rng (q1 - ((s1 - s2) * Ns1)) c= dom (f | Y) by RELAT_1:61;

A33: (s1 - s2) * Ns1 is subsequence of s1 - s2 by VALUED_0:def 17;

then A34: (s1 - s2) * Ns1 is convergent by A32, SEQ_4:16;

lim (s1 - s2) = 0 by A26, A32, SEQ_2:def 7;

then lim ((s1 - s2) * Ns1) = 0 by A32, A33, SEQ_4:17;

then A35: lim (q1 - ((s1 - s2) * Ns1)) = (lim q1) - 0 by A11, A34, SEQ_2:12

.= lim q1 ;

A36: q1 - ((s1 - s2) * Ns1) is convergent by A11, A34, SEQ_2:11;

then A37: (f | Y) /* (q1 - ((s1 - s2) * Ns1)) is convergent by A13, A35, A25, FCONT_1:def 1;

then A38: ((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) is convergent by A17, SEQ_2:11;

(f | Y) . (lim q1) = lim ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) by A13, A36, A35, A25, FCONT_1:def 1;

then A39: lim (((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) = ((f | Y) . (lim q1)) - ((f | Y) . (lim q1)) by A17, A16, A37, SEQ_2:12

.= 0 ;

f | Y is uniformly_continuous

let Y be Subset of REAL; :: thesis: ( Y c= dom f & Y is compact & f | Y is continuous implies f | Y is uniformly_continuous )

assume that

A1: Y c= dom f and

A2: Y is compact and

A3: f | Y is continuous ; :: thesis: f | Y is uniformly_continuous

assume not f | Y is uniformly_continuous ; :: thesis: contradiction

then consider r being Real such that

A4: 0 < r and

A5: for s being Real st 0 < s holds

ex x1, x2 being Real st

( x1 in dom (f | Y) & x2 in dom (f | Y) & |.(x1 - x2).| < s & not |.((f . x1) - (f . x2)).| < r ) by Th1;

defpred S

( x2 in Y & |.($2 - x2).| < 1 / ($1 + 1) & not |.((f . $2) - (f . x2)).| < r ) );

A6: now :: thesis: for n being Element of NAT ex x1 being Element of REAL st S_{1}[n,x1]

consider s1 being Real_Sequence such that let n be Element of NAT ; :: thesis: ex x1 being Element of REAL st S_{1}[n,x1]

consider x1 being Real such that

A7: ex x2 being Real st

( x1 in dom (f | Y) & x2 in dom (f | Y) & |.(x1 - x2).| < 1 / (n + 1) & not |.((f . x1) - (f . x2)).| < r ) by A5, XREAL_1:139;

reconsider x1 = x1 as Element of REAL by XREAL_0:def 1;

take x1 = x1; :: thesis: S_{1}[n,x1]

dom (f | Y) = Y by A1, RELAT_1:62;

hence S_{1}[n,x1]
by A7; :: thesis: verum

end;consider x1 being Real such that

A7: ex x2 being Real st

( x1 in dom (f | Y) & x2 in dom (f | Y) & |.(x1 - x2).| < 1 / (n + 1) & not |.((f . x1) - (f . x2)).| < r ) by A5, XREAL_1:139;

reconsider x1 = x1 as Element of REAL by XREAL_0:def 1;

take x1 = x1; :: thesis: S

dom (f | Y) = Y by A1, RELAT_1:62;

hence S

A8: for n being Element of NAT holds S

now :: thesis: for x being object st x in rng s1 holds

x in Y

then A9:
rng s1 c= Y
by TARSKI:def 3;x in Y

let x be object ; :: thesis: ( x in rng s1 implies x in Y )

assume x in rng s1 ; :: thesis: x in Y

then ex n being Element of NAT st x = s1 . n by FUNCT_2:113;

hence x in Y by A8; :: thesis: verum

end;assume x in rng s1 ; :: thesis: x in Y

then ex n being Element of NAT st x = s1 . n by FUNCT_2:113;

hence x in Y by A8; :: thesis: verum

then consider q1 being Real_Sequence such that

A10: q1 is subsequence of s1 and

A11: q1 is convergent and

A12: lim q1 in Y by A2, RCOMP_1:def 3;

lim q1 in dom (f | Y) by A1, A12, RELAT_1:57;

then A13: f | Y is_continuous_in lim q1 by A3, FCONT_1:def 2;

rng q1 c= rng s1 by A10, VALUED_0:21;

then A14: rng q1 c= Y by A9, XBOOLE_1:1;

then rng q1 c= dom f by A1, XBOOLE_1:1;

then rng q1 c= (dom f) /\ Y by A14, XBOOLE_1:19;

then A15: rng q1 c= dom (f | Y) by RELAT_1:61;

then A16: (f | Y) . (lim q1) = lim ((f | Y) /* q1) by A11, A13, FCONT_1:def 1;

A17: (f | Y) /* q1 is convergent by A11, A13, A15, FCONT_1:def 1;

defpred S

A18: for n being Element of NAT ex x2 being Element of REAL st S

consider s2 being Real_Sequence such that

A19: for n being Element of NAT holds S

now :: thesis: for x being object st x in rng s2 holds

x in Y

then A20:
rng s2 c= Y
by TARSKI:def 3;x in Y

let x be object ; :: thesis: ( x in rng s2 implies x in Y )

assume x in rng s2 ; :: thesis: x in Y

then ex n being Element of NAT st x = s2 . n by FUNCT_2:113;

hence x in Y by A19; :: thesis: verum

end;assume x in rng s2 ; :: thesis: x in Y

then ex n being Element of NAT st x = s2 . n by FUNCT_2:113;

hence x in Y by A19; :: thesis: verum

consider Ns1 being V46() sequence of NAT such that

A21: q1 = s1 * Ns1 by A10, VALUED_0:def 17;

set q2 = q1 - ((s1 - s2) * Ns1);

A22: now :: thesis: for n being Element of NAT holds (q1 - ((s1 - s2) * Ns1)) . n = (s2 * Ns1) . n

then A23:
q1 - ((s1 - s2) * Ns1) = s2 * Ns1
by FUNCT_2:63;let n be Element of NAT ; :: thesis: (q1 - ((s1 - s2) * Ns1)) . n = (s2 * Ns1) . n

thus (q1 - ((s1 - s2) * Ns1)) . n = ((s1 * Ns1) . n) - (((s1 - s2) * Ns1) . n) by A21, RFUNCT_2:1

.= (s1 . (Ns1 . n)) - (((s1 - s2) * Ns1) . n) by FUNCT_2:15

.= (s1 . (Ns1 . n)) - ((s1 - s2) . (Ns1 . n)) by FUNCT_2:15

.= (s1 . (Ns1 . n)) - ((s1 . (Ns1 . n)) - (s2 . (Ns1 . n))) by RFUNCT_2:1

.= (s2 * Ns1) . n by FUNCT_2:15 ; :: thesis: verum

end;thus (q1 - ((s1 - s2) * Ns1)) . n = ((s1 * Ns1) . n) - (((s1 - s2) * Ns1) . n) by A21, RFUNCT_2:1

.= (s1 . (Ns1 . n)) - (((s1 - s2) * Ns1) . n) by FUNCT_2:15

.= (s1 . (Ns1 . n)) - ((s1 - s2) . (Ns1 . n)) by FUNCT_2:15

.= (s1 . (Ns1 . n)) - ((s1 . (Ns1 . n)) - (s2 . (Ns1 . n))) by RFUNCT_2:1

.= (s2 * Ns1) . n by FUNCT_2:15 ; :: thesis: verum

q1 - ((s1 - s2) * Ns1) is subsequence of s2 by A22, FUNCT_2:63, VALUED_0:def 17;

then rng (q1 - ((s1 - s2) * Ns1)) c= rng s2 by VALUED_0:21;

then A24: rng (q1 - ((s1 - s2) * Ns1)) c= Y by A20, XBOOLE_1:1;

then rng (q1 - ((s1 - s2) * Ns1)) c= dom f by A1, XBOOLE_1:1;

then rng (q1 - ((s1 - s2) * Ns1)) c= (dom f) /\ Y by A24, XBOOLE_1:19;

then A25: rng (q1 - ((s1 - s2) * Ns1)) c= dom (f | Y) by RELAT_1:61;

A26: now :: thesis: for p being Real st 0 < p holds

ex k being Nat st

for m being Nat st k <= m holds

|.(((s1 - s2) . m) - 0).| < p

then A32:
s1 - s2 is convergent
by SEQ_2:def 6;ex k being Nat st

for m being Nat st k <= m holds

|.(((s1 - s2) . m) - 0).| < p

let p be Real; :: thesis: ( 0 < p implies ex k being Nat st

for m being Nat st k <= m holds

|.(((s1 - s2) . m) - 0).| < p )

assume A27: 0 < p ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

|.(((s1 - s2) . m) - 0).| < p

consider k being Nat such that

A28: p " < k by SEQ_4:3;

take k = k; :: thesis: for m being Nat st k <= m holds

|.(((s1 - s2) . m) - 0).| < p

let m be Nat; :: thesis: ( k <= m implies |.(((s1 - s2) . m) - 0).| < p )

A29: m in NAT by ORDINAL1:def 12;

assume k <= m ; :: thesis: |.(((s1 - s2) . m) - 0).| < p

then k + 1 <= m + 1 by XREAL_1:6;

then 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;

then A30: |.((s1 . m) - (s2 . m)).| < 1 / (k + 1) by A19, XXREAL_0:2, A29;

k < k + 1 by NAT_1:13;

then p " < k + 1 by A28, XXREAL_0:2;

then 1 / (k + 1) < 1 / (p ") by A27, XREAL_1:76;

then A31: 1 / (k + 1) < p by XCMPLX_1:216;

|.(((s1 - s2) . m) - 0).| = |.((s1 . m) - (s2 . m)).| by RFUNCT_2:1;

hence |.(((s1 - s2) . m) - 0).| < p by A31, A30, XXREAL_0:2; :: thesis: verum

end;for m being Nat st k <= m holds

|.(((s1 - s2) . m) - 0).| < p )

assume A27: 0 < p ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

|.(((s1 - s2) . m) - 0).| < p

consider k being Nat such that

A28: p " < k by SEQ_4:3;

take k = k; :: thesis: for m being Nat st k <= m holds

|.(((s1 - s2) . m) - 0).| < p

let m be Nat; :: thesis: ( k <= m implies |.(((s1 - s2) . m) - 0).| < p )

A29: m in NAT by ORDINAL1:def 12;

assume k <= m ; :: thesis: |.(((s1 - s2) . m) - 0).| < p

then k + 1 <= m + 1 by XREAL_1:6;

then 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;

then A30: |.((s1 . m) - (s2 . m)).| < 1 / (k + 1) by A19, XXREAL_0:2, A29;

k < k + 1 by NAT_1:13;

then p " < k + 1 by A28, XXREAL_0:2;

then 1 / (k + 1) < 1 / (p ") by A27, XREAL_1:76;

then A31: 1 / (k + 1) < p by XCMPLX_1:216;

|.(((s1 - s2) . m) - 0).| = |.((s1 . m) - (s2 . m)).| by RFUNCT_2:1;

hence |.(((s1 - s2) . m) - 0).| < p by A31, A30, XXREAL_0:2; :: thesis: verum

A33: (s1 - s2) * Ns1 is subsequence of s1 - s2 by VALUED_0:def 17;

then A34: (s1 - s2) * Ns1 is convergent by A32, SEQ_4:16;

lim (s1 - s2) = 0 by A26, A32, SEQ_2:def 7;

then lim ((s1 - s2) * Ns1) = 0 by A32, A33, SEQ_4:17;

then A35: lim (q1 - ((s1 - s2) * Ns1)) = (lim q1) - 0 by A11, A34, SEQ_2:12

.= lim q1 ;

A36: q1 - ((s1 - s2) * Ns1) is convergent by A11, A34, SEQ_2:11;

then A37: (f | Y) /* (q1 - ((s1 - s2) * Ns1)) is convergent by A13, A35, A25, FCONT_1:def 1;

then A38: ((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) is convergent by A17, SEQ_2:11;

(f | Y) . (lim q1) = lim ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) by A13, A36, A35, A25, FCONT_1:def 1;

then A39: lim (((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) = ((f | Y) . (lim q1)) - ((f | Y) . (lim q1)) by A17, A16, A37, SEQ_2:12

.= 0 ;

now :: thesis: for n being Element of NAT holds contradiction

hence
contradiction
; :: thesis: verumlet n be Element of NAT ; :: thesis: contradiction

consider k being Nat such that

A40: for m being Nat st k <= m holds

|.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . m) - 0).| < r by A4, A38, A39, SEQ_2:def 7;

A41: q1 . k in rng q1 by VALUED_0:28;

A42: (q1 - ((s1 - s2) * Ns1)) . k in rng (q1 - ((s1 - s2) * Ns1)) by VALUED_0:28;

A43: k in NAT by ORDINAL1:def 12;

|.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k) - 0).| = |.((((f | Y) /* q1) . k) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).| by RFUNCT_2:1

.= |.(((f | Y) . (q1 . k)) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).| by A15, FUNCT_2:108, A43

.= |.(((f | Y) . (q1 . k)) - ((f | Y) . ((q1 - ((s1 - s2) * Ns1)) . k))).| by A25, FUNCT_2:108, A43

.= |.((f . (q1 . k)) - ((f | Y) . ((q1 - ((s1 - s2) * Ns1)) . k))).| by A15, A41, FUNCT_1:47

.= |.((f . (q1 . k)) - (f . ((q1 - ((s1 - s2) * Ns1)) . k))).| by A25, A42, FUNCT_1:47

.= |.((f . (s1 . (Ns1 . k))) - (f . ((s2 * Ns1) . k))).| by A21, A23, FUNCT_2:15, A43

.= |.((f . (s1 . (Ns1 . k))) - (f . (s2 . (Ns1 . k)))).| by FUNCT_2:15, A43 ;

hence contradiction by A19, A40; :: thesis: verum

end;consider k being Nat such that

A40: for m being Nat st k <= m holds

|.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . m) - 0).| < r by A4, A38, A39, SEQ_2:def 7;

A41: q1 . k in rng q1 by VALUED_0:28;

A42: (q1 - ((s1 - s2) * Ns1)) . k in rng (q1 - ((s1 - s2) * Ns1)) by VALUED_0:28;

A43: k in NAT by ORDINAL1:def 12;

|.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k) - 0).| = |.((((f | Y) /* q1) . k) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).| by RFUNCT_2:1

.= |.(((f | Y) . (q1 . k)) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).| by A15, FUNCT_2:108, A43

.= |.(((f | Y) . (q1 . k)) - ((f | Y) . ((q1 - ((s1 - s2) * Ns1)) . k))).| by A25, FUNCT_2:108, A43

.= |.((f . (q1 . k)) - ((f | Y) . ((q1 - ((s1 - s2) * Ns1)) . k))).| by A15, A41, FUNCT_1:47

.= |.((f . (q1 . k)) - (f . ((q1 - ((s1 - s2) * Ns1)) . k))).| by A25, A42, FUNCT_1:47

.= |.((f . (s1 . (Ns1 . k))) - (f . ((s2 * Ns1) . k))).| by A21, A23, FUNCT_2:15, A43

.= |.((f . (s1 . (Ns1 . k))) - (f . (s2 . (Ns1 . k)))).| by FUNCT_2:15, A43 ;

hence contradiction by A19, A40; :: thesis: verum