let CNS be ComplexNormSpace; for RNS being RealNormSpace
for f being PartFunc of RNS,CNS
for x0 being Point of RNS st f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )
let RNS be RealNormSpace; for f being PartFunc of RNS,CNS
for x0 being Point of RNS st f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )
let f be PartFunc of RNS,CNS; for x0 being Point of RNS st f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )
let x0 be Point of RNS; ( f is_continuous_in x0 implies ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 ) )
assume A1:
f is_continuous_in x0
; ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )
then A2:
x0 in dom f
;
now ( 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) ) ) )thus A3:
x0 in dom ||.f.||
by A2, NORMSP_0:def 3;
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) )let s1 be
sequence of
RNS;
( 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 )
;
( ||.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 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;
||.f.|| /. x0 = lim (||.f.|| /* s1)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
;
verum end;
hence
||.f.|| is_continuous_in x0
; - f is_continuous_in x0
- f = (- 1r) (#) f
by VFUNCT_2:23;
hence
- f is_continuous_in x0
by A1, Th37; verum