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
A3: Y c= dom f and
A1: Y is compact and
A2: 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) & abs (x1 - x2) < s & not abs ((f . x1) - (f . x2)) < r ) by Def1;
defpred S₁[ Element of NAT , Real] means ( $2 in Y & ex x2 being Real st
( x2 in Y & abs ($2 - x2) < 1 / ($1 + 1) & not abs ((f . $2) - (f . x2)) < r ) );

A6: now

let n be Element of NAT ; :: thesis: ex x1 being Real st S₁[n,x1]
consider x1 being Real such that
B7: ex x2 being Real st
( x1 in dom (f | Y) & x2 in dom (f | Y) & abs (x1 - x2) < 1 / (n + 1) & not abs ((f . x1) - (f . x2)) < r ) by A5, XREAL_1:141;
dom (f | Y) = Y by A3, RELAT_1:91;
then A7: ex x2 being Real st
( x1 in Y & x2 in Y & abs (x1 - x2) < 1 / (n + 1) & not abs ((f . x1) - (f . x2)) < r ) by B7;
take x1 = x1; :: thesis: S₁[n,x1]
thus S₁[n,x1] by A7; :: thesis: verum

end;

consider s1 being Real_Sequence such that
A8: for n being Element of NAT holds S₁[n,s1 . n] from FUNCT_2:sch 3(A6);
defpred S₂[ Element of NAT , real number ] means ( $2 in Y & abs ((s1 . $1) - $2) < 1 / ($1 + 1) & not abs ((f . (s1 . $1)) - (f . $2)) < r );
A9: for n being Element of NAT ex x2 being Real st S₂[n,x2] by A8;
consider s2 being Real_Sequence such that
A11: for n being Element of NAT holds S₂[n,s2 . n] from FUNCT_2:sch 3(A9);

A12: now

let p be real number ; :: thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((s1 - s2) . m) - 0 ) < p )
assume A13: 0 < p ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((s1 - s2) . m) - 0 ) < p
consider k being Element of NAT such that
A14: p " < k by SEQ_4:10;
A15: 0 < p " by A13;
k < k + 1 by NAT_1:13;
then p " < k + 1 by A14, XXREAL_0:2;
then 1 / (k + 1) < 1 / (p " ) by A15, XREAL_1:78;
then A16: 1 / (k + 1) < p by XCMPLX_1:218;
take k = k; :: thesis: for m being Element of NAT st k <= m holds
abs (((s1 - s2) . m) - 0 ) < p
let m be Element of NAT ; :: thesis: ( k <= m implies abs (((s1 - s2) . m) - 0 ) < p )
assume A17: k <= m ; :: thesis: abs (((s1 - s2) . m) - 0 ) < p
k + 1 <= m + 1 by A17, XREAL_1:8;
then A18: 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:120;
A19: abs (((s1 - s2) . m) - 0 ) = abs ((s1 . m) - (s2 . m)) by RFUNCT_2:6;
abs ((s1 . m) - (s2 . m)) < 1 / (k + 1) by A18, A11, XXREAL_0:2;
hence abs (((s1 - s2) . m) - 0 ) < p by A16, A19, XXREAL_0:2; :: thesis: verum

end;

then A20: s1 - s2 is convergent by SEQ_2:def 6;
then A21: lim (s1 - s2) = 0 by A12, SEQ_2:def 7;

now

let x be set ; :: 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:190;
hence x in Y by A8; :: thesis: verum

end;

then A22: rng s1 c= Y by TARSKI:def 3;
then consider q1 being Real_Sequence such that
A23: ( q1 is subsequence of s1 & q1 is convergent & lim q1 in Y ) by A1, RCOMP_1:def 3;
lim q1 in dom (f | Y) by A23, A3, RELAT_1:86;
then A24: f | Y is_continuous_in lim q1 by A2, FCONT_1:def 2;
consider Ns1 being V34 sequence of NAT such that
A25: q1 = s1 * Ns1 by A23, VALUED_0:def 17;
A26: (s1 - s2) * Ns1 is subsequence of s1 - s2 by VALUED_0:def 17;
then A27: (s1 - s2) * Ns1 is convergent by A20, SEQ_4:29;
A28: lim ((s1 - s2) * Ns1) = 0 by A20, A21, A26, SEQ_4:30;
set q2 = q1 - ((s1 - s2) * Ns1);
A29: q1 - ((s1 - s2) * Ns1) is convergent by A23, A27, SEQ_2:25;
A30: lim (q1 - ((s1 - s2) * Ns1)) = (lim q1) - 0 by A23, A27, A28, SEQ_2:26
.= lim q1 ;

B31: now

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 A25, RFUNCT_2:6
.= (s1 . (Ns1 . n)) - (((s1 - s2) * Ns1) . n) by FUNCT_2:21
.= (s1 . (Ns1 . n)) - ((s1 - s2) . (Ns1 . n)) by FUNCT_2:21
.= (s1 . (Ns1 . n)) - ((s1 . (Ns1 . n)) - (s2 . (Ns1 . n))) by RFUNCT_2:6
.= (s2 * Ns1) . n by FUNCT_2:21 ; :: thesis: verum

end;

then A31: q1 - ((s1 - s2) * Ns1) = s2 * Ns1 by FUNCT_2:113;
A32: q1 - ((s1 - s2) * Ns1) is subsequence of s2 by B31, FUNCT_2:113, VALUED_0:def 17;

now

let x be set ; :: 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:190;
hence x in Y by A11; :: thesis: verum

end;

then A33: rng s2 c= Y by TARSKI:def 3;
rng q1 c= rng s1 by A23, VALUED_0:21;
then A34: rng q1 c= Y by A22, XBOOLE_1:1;
then rng q1 c= dom f by A3, XBOOLE_1:1;
then rng q1 c= (dom f) /\ Y by A34, XBOOLE_1:19;
then A35: rng q1 c= dom (f | Y) by RELAT_1:90;
then A36: ( (f | Y) /* q1 is convergent & (f | Y) . (lim q1) = lim ((f | Y) /* q1) ) by A23, A24, FCONT_1:def 1;
rng (q1 - ((s1 - s2) * Ns1)) c= rng s2 by A32, VALUED_0:21;
then A37: rng (q1 - ((s1 - s2) * Ns1)) c= Y by A33, XBOOLE_1:1;
then rng (q1 - ((s1 - s2) * Ns1)) c= dom f by A3, XBOOLE_1:1;
then rng (q1 - ((s1 - s2) * Ns1)) c= (dom f) /\ Y by A37, XBOOLE_1:19;
then A38: rng (q1 - ((s1 - s2) * Ns1)) c= dom (f | Y) by RELAT_1:90;
then A39: ( (f | Y) /* (q1 - ((s1 - s2) * Ns1)) is convergent & (f | Y) . (lim q1) = lim ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) ) by A24, A29, A30, FCONT_1:def 1;
then A40: ((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) is convergent by A36, SEQ_2:25;
A41: lim (((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) = ((f | Y) . (lim q1)) - ((f | Y) . (lim q1)) by A36, A39, SEQ_2:26
.= 0 ;

now

let n be Element of NAT ; :: thesis: contradiction
consider k being Element of NAT such that
A42: for m being Element of NAT st k <= m holds
abs (((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . m) - 0 ) < r by A4, A40, A41, SEQ_2:def 7;
A44: q1 . k in rng q1 by VALUED_0:28;
A45: (q1 - ((s1 - s2) * Ns1)) . k in rng (q1 - ((s1 - s2) * Ns1)) by VALUED_0:28;
abs (((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k) - 0 ) = abs ((((f | Y) /* q1) . k) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)) by RFUNCT_2:6
.= abs (((f | Y) . (q1 . k)) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)) by A35, FUNCT_2:185
.= abs (((f | Y) . (q1 . k)) - ((f | Y) . ((q1 - ((s1 - s2) * Ns1)) . k))) by A38, FUNCT_2:185
.= abs ((f . (q1 . k)) - ((f | Y) . ((q1 - ((s1 - s2) * Ns1)) . k))) by A35, A44, FUNCT_1:68
.= abs ((f . (q1 . k)) - (f . ((q1 - ((s1 - s2) * Ns1)) . k))) by A38, A45, FUNCT_1:68
.= abs ((f . (s1 . (Ns1 . k))) - (f . ((s2 * Ns1) . k))) by A25, A31, FUNCT_2:21
.= abs ((f . (s1 . (Ns1 . k))) - (f . (s2 . (Ns1 . k)))) by FUNCT_2:21 ;
hence contradiction by A11, A42; :: thesis: verum

end;

hence contradiction ; :: thesis: verum