let CNS1, CNS2 be ComplexNormSpace; :: thesis: for X being set
for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
f is_continuous_on X
let X be set ; :: thesis: for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
f is_continuous_on X
let f be PartFunc of CNS1,CNS2; :: 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 & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) ) by Def27;
A3: X c= dom f by A1, Def27;
then A4: dom (f | X) = X by RELAT_1:91;

now

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

now

let g be Real; :: thesis: ( 0 < g implies ex s' being Element of REAL st
( 0 < s' & ( for x1 being Point of CNS1 st x1 in dom (f | X) & ||.(x1 - x0).|| < s' holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g ) ) )
assume A6: 0 < g ; :: thesis: ex s' being Element of REAL st
( 0 < s' & ( for x1 being Point of CNS1 st x1 in dom (f | X) & ||.(x1 - x0).|| < s' holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g ) )
set s = g / r;
take s' = g / r; :: thesis: ( 0 < s' & ( for x1 being Point of CNS1 st x1 in dom (f | X) & ||.(x1 - x0).|| < s' holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g ) )
A7: 0 < r " by A2, XREAL_1:124;
A8: s' = g * (r " ) by XCMPLX_0:def 9;

now

let x1 be Point of CNS1; :: thesis: ( x1 in dom (f | X) & ||.(x1 - x0).|| < g / r implies ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g )
assume A9: ( x1 in dom (f | X) & ||.(x1 - x0).|| < g / r ) ; :: thesis: ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g
then r * ||.(x1 - x0).|| < (g / r) * r by A2, XREAL_1:70;
then A10: r * ||.(x1 - x0).|| < g by A2, XCMPLX_1:88;
||.((f /. x1) - (f /. x0)).|| <= r * ||.(x1 - x0).|| by A2, A4, A5, A9;
then ||.((f /. x1) - (f /. x0)).|| < g by A10, XXREAL_0:2;
then ||.(((f | X) /. x1) - (f /. x0)).|| < g by A9, PARTFUN2:32;
hence ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g by A4, A5, PARTFUN2:32; :: thesis: verum

end;

hence ( 0 < s' & ( for x1 being Point of CNS1 st x1 in dom (f | X) & ||.(x1 - x0).|| < s' holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g ) ) by A6, A7, A8, XREAL_1:131; :: thesis: verum

end;

hence f | X is_continuous_in x0 by A4, A5, Th29; :: thesis: verum

end;

hence f is_continuous_on X by A3, Def21; :: thesis: verum