let X be set ; :: thesis: for S being RealNormSpace
for f being PartFunc of the carrier of S,REAL st f is_Lipschitzian_on X holds
f is_continuous_on X
let S be RealNormSpace; :: thesis: for f being PartFunc of the carrier of S,REAL st f is_Lipschitzian_on X holds
f is_continuous_on X
let f be PartFunc of the carrier of S,REAL; :: thesis: ( f is_Lipschitzian_on X implies f is_continuous_on X )
assume A1: f is_Lipschitzian_on X ; :: thesis: f is_continuous_on X
then consider r being Real such that
A2: 0 < r and
A3: for x1, x2 being Point of S st x1 in X & x2 in X holds
|.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| ;
A4: X c= dom f by A1;
then A5: dom (f | X) = X by RELAT_1:62;

now :: thesis: for x0 being Point of S st x0 in X holds
f | X is_continuous_in x0

let x0 be Point of S; :: thesis: ( x0 in X implies f | X is_continuous_in x0 )
assume A6: x0 in X ; :: thesis: f | X is_continuous_in x0

now :: thesis: for g being Real st 0 < g holds
ex s9 being Real st
( 0 < s9 & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < g ) )

let g be Real; :: thesis: ( 0 < g implies ex s9 being Real st
( 0 < s9 & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < g ) ) )
assume A7: 0 < g ; :: thesis: ex s9 being Real st
( 0 < s9 & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < g ) )
reconsider s = g / r as Real ;
take s9 = s; :: thesis: ( 0 < s9 & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < g ) )

A8: now :: thesis: for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < g

let x1 be Point of S; :: thesis: ( x1 in dom (f | X) & ||.(x1 - x0).|| < s implies |.(((f | X) /. x1) - ((f | X) /. x0)).| < g )
assume that
A9: x1 in dom (f | X) and
A10: ||.(x1 - x0).|| < s ; :: thesis: |.(((f | X) /. x1) - ((f | X) /. x0)).| < g
r * ||.(x1 - x0).|| < (g / r) * r by A2, A10, XREAL_1:68;
then A11: r * ||.(x1 - x0).|| < g by A2, XCMPLX_1:87;
|.((f /. x1) - (f /. x0)).| <= r * ||.(x1 - x0).|| by A3, A5, A6, A9;
then |.((f /. x1) - (f /. x0)).| < g by A11, XXREAL_0:2;
then |.(((f | X) /. x1) - (f /. x0)).| < g by A9, PARTFUN2:15;
hence |.(((f | X) /. x1) - ((f | X) /. x0)).| < g by A5, A6, PARTFUN2:15; :: thesis: verum

end;

( 0 < r " & s9 = g * (r ") ) by A2, XCMPLX_0:def 9;
hence ( 0 < s9 & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < g ) ) by A7, A8, XREAL_1:129; :: thesis: verum

end;

hence f | X is_continuous_in x0 by A5, A6, Th8; :: thesis: verum

end;

hence f is_continuous_on X by A4; :: thesis: verum