let CNS1, CNS2 be ComplexNormSpace; :: thesis: for f being PartFunc of CNS1,CNS2
for x0 being Point of CNS1 st f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )
let f be PartFunc of CNS1,CNS2; :: thesis: for x0 being Point of CNS1 st f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )
let x0 be Point of CNS1; :: thesis: ( f is_continuous_in x0 implies ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 ) )
assume A1: f is_continuous_in x0 ; :: thesis: ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )
then A2: ( x0 in dom f & ( for s1 being sequence of CNS1 st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) by Def15;

now

thus A3: x0 in dom ||.f.|| by A2, Def2; :: thesis: for s1 being sequence of CNS1 st rng s1 c= dom ||.f.|| & s1 is convergent & lim s1 = x0 holds
( ||.f.|| /* s1 is convergent & ||.f.|| /. x0 = lim (||.f.|| /* s1) )
let s1 be sequence of CNS1; :: thesis: ( rng s1 c= dom ||.f.|| & s1 is convergent & lim s1 = x0 implies ( ||.f.|| /* s1 is convergent & ||.f.|| /. x0 = lim (||.f.|| /* s1) ) )
assume A4: ( rng s1 c= dom ||.f.|| & s1 is convergent & lim s1 = x0 ) ; :: thesis: ( ||.f.|| /* s1 is convergent & ||.f.|| /. x0 = lim (||.f.|| /* s1) )
then A5: rng s1 c= dom f by Def2;
then A6: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A4, Def15;
then ||.(f /* s1).|| is convergent by CLVECT_1:119;
hence ||.f.|| /* s1 is convergent by A5, Th50; :: thesis: ||.f.|| /. x0 = lim (||.f.|| /* s1)
thus ||.f.|| /. x0 = ||.f.|| . x0 by A3, PARTFUN1:def 8
.= ||.(f /. x0).|| by A3, Def2
.= lim ||.(f /* s1).|| by A6, CLOPBAN1:45
.= lim (||.f.|| /* s1) by A5, Th50 ; :: thesis: verum

end;

hence ||.f.|| is_continuous_in x0 by Def19; :: thesis: - f is_continuous_in x0
- f = (- 1r ) (#) f by VFUNCT_2:23;
hence - f is_continuous_in x0 by A1, Th56; :: thesis: verum