let g, x0 be Complex; for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 holds
g (#) f is_continuous_in x0
let f be PartFunc of COMPLEX,COMPLEX; ( f is_continuous_in x0 implies g (#) f is_continuous_in x0 )
assume A1:
f is_continuous_in x0
; g (#) f is_continuous_in x0
then
x0 in dom f
;
hence A2:
x0 in dom (g (#) f)
by VALUED_1:def 5; CFCONT_1:def 1 for s1 being Complex_Sequence st rng s1 c= dom (g (#) f) & s1 is convergent & lim s1 = x0 holds
( (g (#) f) /* s1 is convergent & (g (#) f) /. x0 = lim ((g (#) f) /* s1) )
let s1 be Complex_Sequence; ( rng s1 c= dom (g (#) f) & s1 is convergent & lim s1 = x0 implies ( (g (#) f) /* s1 is convergent & (g (#) f) /. x0 = lim ((g (#) f) /* s1) ) )
assume that
A3:
rng s1 c= dom (g (#) f)
and
A4:
( s1 is convergent & lim s1 = x0 )
; ( (g (#) f) /* s1 is convergent & (g (#) f) /. x0 = lim ((g (#) f) /* s1) )
A5:
rng s1 c= dom f
by A3, VALUED_1:def 5;
then A6:
f /. x0 = lim (f /* s1)
by A1, A4;
A7:
f /* s1 is convergent
by A1, A4, A5;
then
g (#) (f /* s1) is convergent
;
hence
(g (#) f) /* s1 is convergent
by A5, Th8; (g (#) f) /. x0 = lim ((g (#) f) /* s1)
thus (g (#) f) /. x0 =
g * (f /. x0)
by A2, CFUNCT_1:4
.=
lim (g (#) (f /* s1))
by A7, A6, COMSEQ_2:18
.=
lim ((g (#) f) /* s1)
by A5, Th8
; verum