let CNS be ComplexNormSpace; for RNS being RealNormSpace
for f being PartFunc of RNS,CNS
for x0 being Point of RNS
for z being Complex st f is_continuous_in x0 holds
z (#) f is_continuous_in x0
let RNS be RealNormSpace; for f being PartFunc of RNS,CNS
for x0 being Point of RNS
for z being Complex st f is_continuous_in x0 holds
z (#) f is_continuous_in x0
let f be PartFunc of RNS,CNS; for x0 being Point of RNS
for z being Complex st f is_continuous_in x0 holds
z (#) f is_continuous_in x0
let x0 be Point of RNS; for z being Complex st f is_continuous_in x0 holds
z (#) f is_continuous_in x0
let z be Complex; ( f is_continuous_in x0 implies z (#) f is_continuous_in x0 )
assume A1:
f is_continuous_in x0
; z (#) f is_continuous_in x0
then
x0 in dom f
;
hence A2:
x0 in dom (z (#) f)
by VFUNCT_2:def 2; NCFCONT1:def 7 for seq being sequence of RNS st rng seq c= dom (z (#) f) & seq is convergent & lim seq = x0 holds
( (z (#) f) /* seq is convergent & (z (#) f) /. x0 = lim ((z (#) f) /* seq) )
let s1 be sequence of RNS; ( rng s1 c= dom (z (#) f) & s1 is convergent & lim s1 = x0 implies ( (z (#) f) /* s1 is convergent & (z (#) f) /. x0 = lim ((z (#) f) /* s1) ) )
assume that
A3:
rng s1 c= dom (z (#) f)
and
A4:
( s1 is convergent & lim s1 = x0 )
; ( (z (#) f) /* s1 is convergent & (z (#) f) /. x0 = lim ((z (#) f) /* s1) )
A5:
rng s1 c= dom f
by A3, VFUNCT_2:def 2;
then A6:
f /. x0 = lim (f /* s1)
by A1, A4;
A7:
f /* s1 is convergent
by A1, A4, A5;
then
z * (f /* s1) is convergent
by CLVECT_1:116;
hence
(z (#) f) /* s1 is convergent
by A5, Th28; (z (#) f) /. x0 = lim ((z (#) f) /* s1)
thus (z (#) f) /. x0 =
z * (f /. x0)
by A2, VFUNCT_2:def 2
.=
lim (z * (f /* s1))
by A7, A6, CLVECT_1:122
.=
lim ((z (#) f) /* s1)
by A5, Th28
; verum