let CNS be ComplexNormSpace; :: thesis: for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for x0 being Point of CNS
for r being Real st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let RNS be RealNormSpace; :: thesis: for f being PartFunc of CNS,RNS
for x0 being Point of CNS
for r being Real st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let f be PartFunc of CNS,RNS; :: thesis: for x0 being Point of CNS
for r being Real st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let x0 be Point of CNS; :: thesis: for r being Real st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let r be Real; :: thesis: ( f is_continuous_in x0 implies r (#) f is_continuous_in x0 )
assume A1: f is_continuous_in x0 ; :: thesis: r (#) f is_continuous_in x0
then x0 in dom f by Def16;
hence A2: x0 in dom (r (#) f) by VFUNCT_1:def 4; :: according to NCFCONT1:def 6 :: thesis: for seq being sequence of CNS st rng seq c= dom (r (#) f) & seq is convergent & lim seq = x0 holds
( (r (#) f) /* seq is convergent & (r (#) f) /. x0 = lim ((r (#) f) /* seq) )
let s1 be sequence of CNS; :: thesis: ( rng s1 c= dom (r (#) f) & s1 is convergent & lim s1 = x0 implies ( (r (#) f) /* s1 is convergent & (r (#) f) /. x0 = lim ((r (#) f) /* s1) ) )
assume that
A3: rng s1 c= dom (r (#) f) and
A4: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) /. x0 = lim ((r (#) f) /* s1) )
A5: rng s1 c= dom f by A3, VFUNCT_1:def 4;
then A6: f /. x0 = lim (f /* s1) by A1, A4, Def16;
A7: f /* s1 is convergent by A1, A4, A5, Def16;
then r * (f /* s1) is convergent by NORMSP_1:22;
hence (r (#) f) /* s1 is convergent by A5, Th48; :: thesis: (r (#) f) /. x0 = lim ((r (#) f) /* s1)
thus (r (#) f) /. x0 = r * (f /. x0) by A2, VFUNCT_1:def 4
.= lim (r * (f /* s1)) by A7, A6, NORMSP_1:28
.= lim ((r (#) f) /* s1) by A5, Th48 ; :: thesis: verum