let CNS1, CNS2 be ComplexNormSpace; :: thesis: for f being PartFunc of CNS1,CNS2
for x0 being Point of CNS1
for z being Complex st f is_continuous_in x0 holds
z (#) f is_continuous_in x0
let f be PartFunc of CNS1,CNS2; :: thesis: for x0 being Point of CNS1
for z being Complex st f is_continuous_in x0 holds
z (#) f is_continuous_in x0
let x0 be Point of CNS1; :: thesis: for z being Complex st f is_continuous_in x0 holds
z (#) f is_continuous_in x0
let z be Complex; :: thesis: ( f is_continuous_in x0 implies z (#) f is_continuous_in x0 )
assume A1: f is_continuous_in x0 ; :: thesis: z (#) f is_continuous_in x0
then x0 in dom f ;
hence A2: x0 in dom (z (#) f) by VFUNCT_2:def 2; :: according to NCFCONT1:def 5 :: thesis: for seq being sequence of CNS1 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 CNS1; :: thesis: ( 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 ) ; :: thesis: ( (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, Th26; :: thesis: (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, Th26 ; :: thesis: verum