let CNS be ComplexNormSpace; :: thesis: for f being PartFunc of CNS,CNS st ( for x0 being Point of CNS st x0 in dom f holds
f /. x0 = x0 ) holds
f is_continuous_on dom f
let f be PartFunc of CNS,CNS; :: thesis: ( ( for x0 being Point of CNS st x0 in dom f holds
f /. x0 = x0 ) implies f is_continuous_on dom f )
assume A1: for x0 being Point of CNS st x0 in dom f holds
f /. x0 = x0 ; :: thesis: f is_continuous_on dom f

now

let x1, x2 be Point of CNS; :: thesis: ( x1 in dom f & x2 in dom f implies ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).||
then ( f /. x1 = x1 & f /. x2 = x2 ) by A1;
hence ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| ; :: thesis: verum

end;

then f is_Lipschitzian_on dom f by Def27;
hence f is_continuous_on dom f by Th137; :: thesis: verum