let CNS be ComplexNormSpace; :: thesis: for f being PartFunc of the carrier of CNS,REAL 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 the carrier of CNS,REAL ; :: 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 abs ((f /. x1) - (f /. x2)) <= 1 * ||.(x1 - x2).|| )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: abs ((f /. x1) - (f /. x2)) <= 1 * ||.(x1 - x2).||
then A2: ( f /. x1 = ||.x1.|| & f /. x2 = ||.x2.|| ) by A1;
A3: ||.x1.|| - ||.x2.|| <= ||.(x1 - x2).|| by CLVECT_1:110;
||.x2.|| - ||.x1.|| <= ||.(x2 - x1).|| by CLVECT_1:110;
then ||.x2.|| - ||.x1.|| <= ||.(x1 - x2).|| by CLVECT_1:109;
then - (- (||.x1.|| - ||.x2.||)) >= - ||.(x1 - x2).|| by XREAL_1:26;
hence abs ((f /. x1) - (f /. x2)) <= 1 * ||.(x1 - x2).|| by A2, A3, ABSVALUE:12; :: thesis: verum

end;

then f is_Lipschitzian_on dom f by Def31;
hence f is_continuous_on dom f by Th141; :: thesis: verum