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 :: thesis: for x1, x2 being Point of CNS st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= 1 * ||.(x1 - x2).||
let x1, x2 be Point of CNS; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f /. x1) - (f /. x2)).| <= 1 * ||.(x1 - x2).|| )
||.x2.|| - ||.x1.|| <= ||.(x2 - x1).|| by CLVECT_1:109;
then ||.x2.|| - ||.x1.|| <= ||.(x1 - x2).|| by CLVECT_1:108;
then A2: ( ||.x1.|| - ||.x2.|| <= ||.(x1 - x2).|| & - (- (||.x1.|| - ||.x2.||)) >= - ||.(x1 - x2).|| ) by CLVECT_1:109, XREAL_1:24;
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).|| by A2, ABSVALUE:5; :: thesis: verum
end;
then f is_Lipschitzian_on dom f ;
hence f is_continuous_on dom f by Th120; :: thesis: verum