let T, S be RealNormSpace; :: thesis: for f being PartFunc of S,T
for x0 being Point of S st f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )
let f be PartFunc of S,T; :: thesis: for x0 being Point of S st f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )
let x0 be Point of S; :: 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 S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) by Def9;

now

thus A3: x0 in dom ||.f.|| by A2, Def2; :: thesis: for s1 being sequence of S 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 S; :: 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, Def9;
then ||.(f /* s1).|| is convergent by NORMSP_1:39;
hence ||.f.|| /* s1 is convergent by A5, Th21; :: 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, LOPBAN_1:47
.= lim (||.f.|| /* s1) by A5, Th21 ; :: thesis: verum

end;

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