let g be Complex; :: thesis: for X being set
for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X holds
g (#) f is_continuous_on X
let X be set ; :: thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X holds
g (#) f is_continuous_on X
let f be PartFunc of COMPLEX,COMPLEX; :: thesis: ( f is_continuous_on X implies g (#) f is_continuous_on X )
assume A1: f is_continuous_on X ; :: thesis: g (#) f is_continuous_on X
then A2: X c= dom f ;
then A3: X c= dom (g (#) f) by CFUNCT_1:4;
now :: thesis: for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( (g (#) f) /* s1 is convergent & (g (#) f) /. (lim s1) = lim ((g (#) f) /* s1) )
let s1 be Complex_Sequence; :: thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (g (#) f) /* s1 is convergent & (g (#) f) /. (lim s1) = lim ((g (#) f) /* s1) ) )
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X ; :: thesis: ( (g (#) f) /* s1 is convergent & (g (#) f) /. (lim s1) = lim ((g (#) f) /* s1) )
A7: f /* s1 is convergent by A1, A4, A5, A6, Th38;
then A8: g (#) (f /* s1) is convergent ;
A9: lim s1 in dom (g (#) f) by A3, A6;
f /. (lim s1) = lim (f /* s1) by A1, A4, A5, A6, Th38;
then (g (#) f) /. (lim s1) = g * (lim (f /* s1)) by CFUNCT_1:4, A9
.= lim (g (#) (f /* s1)) by A7, COMSEQ_2:18
.= lim ((g (#) f) /* s1) by A2, A4, Th8, XBOOLE_1:1 ;
hence ( (g (#) f) /* s1 is convergent & (g (#) f) /. (lim s1) = lim ((g (#) f) /* s1) ) by A2, A4, A8, Th8, XBOOLE_1:1; :: thesis: verum
end;
hence g (#) f is_continuous_on X by A3, Th38; :: thesis: verum