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 ;

thus A3: x0 in dom ||.f.|| by A2, NORMSP_0:def 3; :: thesis:
let s1 be sequence of RNS; :: thesis:
assume that
A4: rng s1 c= dom ||.f.|| and
A5: ( s1 is convergent & lim s1 = x0 ) ; :: thesis:
A6: rng s1 c= dom f by A4, NORMSP_0:def 3;
then A7: f /. x0 = lim (f /* s1) by A1, A5;
A8: f /* s1 is convergent by A1, A5, A6;
then ||.(f /* s1).|| is convergent by CLVECT_1:117;
hence ||.f.|| /* s1 is convergent by A6, Th31; :: thesis:
thus ||.f.|| /. x0 = ||.f.|| . x0 by A3, PARTFUN1:def 6
.= ||.(f /. x0).|| by A3, NORMSP_0:def 3
.= lim ||.(f /* s1).|| by A8, A7, CLOPBAN1:40
.= lim (||.f.|| /* s1) by A6, Th31 ; :: thesis:

end;

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