let x0 be real number ; :: thesis: for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st x0 in dom f & f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )
let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S st x0 in dom f & f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )
let f be PartFunc of REAL, the carrier of S; :: thesis: ( x0 in dom f & f is_continuous_in x0 implies ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 ) )
assume A1: x0 in dom f ; :: thesis: ( not f is_continuous_in x0 or ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 ) )
assume A2: f is_continuous_in x0 ; :: thesis: ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )
Y0: x0 in dom ||.f.|| by A1, NORMSP_0:def 3;

now

let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom ||.f.|| & s1 is convergent & lim s1 = x0 implies ( ||.f.|| /* s1 is convergent & ||.f.|| . x0 = lim (||.f.|| /* s1) ) )
assume that
A3: rng s1 c= dom ||.f.|| and
A4: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( ||.f.|| /* s1 is convergent & ||.f.|| . x0 = lim (||.f.|| /* s1) )
A5: rng s1 c= dom f by A3, NORMSP_0:def 3;
then A6: f /. x0 = lim (f /* s1) by A2, A4, Def1;
A7: f /* s1 is convergent by A2, A4, A5, Def1;
then ||.(f /* s1).|| is convergent by NORMSP_1:39;
hence ||.f.|| /* s1 is convergent by A5, XTh21; :: thesis: ||.f.|| . x0 = lim (||.f.|| /* s1)
thus ||.f.|| . x0 = ||.(f /. x0).|| by Y0, NORMSP_0:def 3
.= lim ||.(f /* s1).|| by A7, A6, LOPBAN_1:24
.= lim (||.f.|| /* s1) by A5, XTh21 ; :: thesis: verum

end;

hence ||.f.|| is_continuous_in x0 by FCONT_1:def 1; :: thesis: - f is_continuous_in x0
(- 1) (#) f is_continuous_in x0 by A2, Th8;
hence - f is_continuous_in x0 by VFUNCT_1:29; :: thesis: verum