let CNS be ComplexNormSpace; :: thesis:
let RNS be RealNormSpace; :: thesis:
let f be PartFunc of CNS,RNS; :: thesis:
let x0 be Point of CNS; :: thesis:
assume A1: f is_continuous_in x0 ; :: thesis:
then A2: ( x0 in dom f & ( for s1 being sequence of CNS st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) by Def16;

thus A3: x0 in dom ||.f.|| by A2, Def3; :: thesis:
let s1 be sequence of CNS; :: thesis:
assume A4: ( rng s1 c= dom ||.f.|| & s1 is convergent & lim s1 = x0 ) ; :: thesis:
then A5: rng s1 c= dom f by Def3;
then A6: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A4, Def16;
then ||.(f /* s1).|| is convergent by NORMSP_1:39;
hence ||.f.|| /* s1 is convergent by A5, Th51; :: thesis:
thus ||.f.|| /. x0 = ||.f.|| . x0 by A3, PARTFUN1:def 8
.= ||.(f /. x0).|| by A3, Def3
.= lim ||.(f /* s1).|| by A6, LOPBAN_1:47
.= lim (||.f.|| /* s1) by A5, Th51 ; :: thesis:

end;

hence ||.f.|| is_continuous_in x0 by Def19; :: thesis:
- f = (- 1) (#) f by VFUNCT_1:29;
hence - f is_continuous_in x0 by A1, Th57; :: thesis: