let x0 be Real; :: 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 )
A3: x0 in dom ||.f.|| by A1, NORMSP_0:def 3;

now :: thesis: for s1 being Real_Sequence 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 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
A4: rng s1 c= dom ||.f.|| and
A5: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( ||.f.|| /* s1 is convergent & ||.f.|| . x0 = lim (||.f.|| /* s1) )
A6: rng s1 c= dom f by A4, NORMSP_0:def 3;
then A7: f /. x0 = lim (f /* s1) by A2, A5;
A8: f /* s1 is convergent by A2, A5, A6;
then ||.(f /* s1).|| is convergent by NORMSP_1:23;
hence ||.f.|| /* s1 is convergent by A6, Th5; :: thesis: ||.f.|| . x0 = lim (||.f.|| /* s1)
thus ||.f.|| . x0 = ||.(f /. x0).|| by A3, NORMSP_0:def 3
.= lim ||.(f /* s1).|| by A8, A7, LOPBAN_1:20
.= lim (||.f.|| /* s1) by A6, Th5 ; :: thesis: verum

end;

hence ||.f.|| is_continuous_in x0 ; :: thesis: - f is_continuous_in x0
(- 1) (#) f is_continuous_in x0 by A2, Th13;
hence - f is_continuous_in x0 by VFUNCT_1:23; :: thesis: verum