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

thus A3: x0 in dom ||.f.|| by A2, Def4; :: thesis:
let s1 be sequence of RNS; :: thesis:
assume A4: ( rng s1 c= dom ||.f.|| & s1 is convergent & lim s1 = x0 ) ; :: thesis:
then A5: rng s1 c= dom f by Def4;
then A6: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A4, Def17;
then ||.(f /* s1).|| is convergent by CLVECT_1:119;
hence ||.f.|| /* s1 is convergent by A5, Th52; :: thesis:
thus ||.f.|| /. x0 = ||.f.|| . x0 by A3, PARTFUN1:def 8
.= ||.(f /. x0).|| by A3, Def4
.= lim ||.(f /* s1).|| by A6, CLOPBAN1:45
.= lim (||.f.|| /* s1) by A5, Th52 ; :: thesis:

end;

hence ||.f.|| is_continuous_in x0 by NFCONT_1:def 10; :: thesis:
- f = (- 1r ) (#) f by VFUNCT_2:23;
hence - f is_continuous_in x0 by A1, Th58; :: thesis: