let X be set ; :: thesis: for f being PartFunc of REAL,REAL st f | X is Lipschitzian holds
f | X is uniformly_continuous
let f be PartFunc of REAL,REAL; :: thesis: ( f | X is Lipschitzian implies f | X is uniformly_continuous )
assume f | X is Lipschitzian ; :: thesis: f | X is uniformly_continuous
then consider r being real number such that
A1: 0 < r and
A2: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) by FCONT_1:33;

now

reconsider r = r as Real by XREAL_0:def 1;
let p be Real; :: thesis: ( 0 < p implies ex s being Element of REAL st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < p ) ) )
assume A3: 0 < p ; :: thesis: ex s being Element of REAL st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < p ) )
take s = p / r; :: thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < p ) )
thus 0 < s by A1, A3, XREAL_1:141; :: thesis: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < p
let x1, x2 be Real; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s implies abs ((f . x1) - (f . x2)) < p )
assume that
A4: x1 in dom (f | X) and
A5: x2 in dom (f | X) and
A6: abs (x1 - x2) < s ; :: thesis: abs ((f . x1) - (f . x2)) < p
A7: r * (abs (x1 - x2)) < s * r by A1, A6, XREAL_1:70;
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) by A2, A4, A5;
then abs ((f . x1) - (f . x2)) < (p / r) * r by A7, XXREAL_0:2;
hence abs ((f . x1) - (f . x2)) < p by A1, XCMPLX_1:88; :: thesis: verum

end;

hence f | X is uniformly_continuous by Th1; :: thesis: verum