let CNS be ComplexNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: 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 & ( 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) ) ) ) by Def17;
hence A2: x0 in dom (z (#) f) by VFUNCT_2:def 4; :: according to NCFCONT1:def 17 :: thesis: 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; :: 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 A3: ( rng s1 c= dom (z (#) f) & s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (z (#) f) /* s1 is convergent & (z (#) f) /. x0 = lim ((z (#) f) /* s1) )
then A4: rng s1 c= dom f by VFUNCT_2:def 4;
then A5: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A3, Def17;
then z * (f /* s1) is convergent by CLVECT_1:118;
hence (z (#) f) /* s1 is convergent by A4, Th49; :: thesis: (z (#) f) /. x0 = lim ((z (#) f) /* s1)
thus (z (#) f) /. x0 = z * (f /. x0) by A2, VFUNCT_2:def 4
.= lim (z * (f /* s1)) by A5, CLVECT_1:124
.= lim ((z (#) f) /* s1) by A4, Th49 ; :: thesis: verum