let g, x0 be Complex; :: thesis: 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; :: thesis: ( f is_continuous_in x0 implies g (#) f is_continuous_in x0 )
assume A1: f is_continuous_in x0 ; :: thesis: g (#) f is_continuous_in x0
then x0 in dom f ;
hence A2: x0 in dom (g (#) f) by VALUED_1:def 5; :: according to CFCONT_1:def 1 :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( (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; :: thesis: (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 ; :: thesis: verum