let g be Element of 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 by Th60;
then A3: X c= dom (g (#) f) by CFUNCT_1:7;

now

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 A4: ( rng s1 c= X & s1 is convergent & lim s1 in X ) ; :: thesis: ( (g (#) f) /* s1 is convergent & (g (#) f) /. (lim s1) = lim ((g (#) f) /* s1) )
then A5: ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) by A1, Th60;
then A6: g (#) (f /* s1) is convergent by COMSEQ_2:17;
(g (#) f) /. (lim s1) = g * (lim (f /* s1)) by A3, A4, A5, CFUNCT_1:7
.= lim (g (#) (f /* s1)) by A5, COMSEQ_2:18
.= lim ((g (#) f) /* s1) by A2, A4, Th19, XBOOLE_1:1 ;
hence ( (g (#) f) /* s1 is convergent & (g (#) f) /. (lim s1) = lim ((g (#) f) /* s1) ) by A2, A4, A6, Th19, XBOOLE_1:1; :: thesis: verum

end;

hence g (#) f is_continuous_on X by A3, Th60; :: thesis: verum