let X be non empty TopSpace; :: thesis: for a being complex number
for f being continuous Function of the carrier of X,COMPLEX holds a (#) f is continuous Function of the carrier of X,COMPLEX
let a be complex number ; :: thesis: for f being continuous Function of the carrier of X,COMPLEX holds a (#) f is continuous Function of the carrier of X,COMPLEX
let f be continuous Function of the carrier of X,COMPLEX; :: thesis: a (#) f is continuous Function of the carrier of X,COMPLEX
set h = a (#) f;
A1: for x being Point of X holds (a (#) f) . x = a * (f . x) by VALUED_1:6;

now

per cases ( a <> 0 or a = 0 ) ;

suppose L1: a <> 0 ; :: thesis: a (#) f is continuous

for p being Point of X
for V being Subset of COMPLEX st (a (#) f) . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & (a (#) f) .: W c= V )

proof

let p be Point of X; :: thesis: for V being Subset of COMPLEX st (a (#) f) . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & (a (#) f) .: W c= V )
let V be Subset of COMPLEX; :: thesis: ( (a (#) f) . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & (a (#) f) .: W c= V ) )
assume A2: ( (a (#) f) . p in V & V is open ) ; :: thesis: ex W being Subset of X st
( p in W & W is open & (a (#) f) .: W c= V )
reconsider z0 = (a (#) f) . p as Complex ;
consider N being Neighbourhood of z0 such that
A3: N c= V by A2, CFDIFF_1:9;
consider r being Real such that
A4: ( 0 < r & { y where y is Complex : |.(y - z0).| < r } c= N ) by CFDIFF_1:def 5;
set S = { y where y is Complex : |.(y - z0).| < r } ;
A5: |.a.| > 0 by L1;
A6: r / |.a.| is Real by XREAL_0:def 1;
A7: r / |.a.| > 0 by L1, A4;
reconsider z1 = f . p as Complex ;
set S1 = { y where y is Complex : |.(y - z1).| < r / |.a.| } ;
{ y where y is Complex : |.(y - z1).| < r / |.a.| } c= COMPLEX

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { y where y is Complex : |.(y - z1).| < r / |.a.| } or z in COMPLEX )
assume z in { y where y is Complex : |.(y - z1).| < r / |.a.| } ; :: thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - z1).| < r / |.a.| ) ;
hence z in COMPLEX ; :: thesis: verum

end;

then reconsider T1 = { y where y is Complex : |.(y - z1).| < r / |.a.| } as Subset of COMPLEX ;
A8: T1 is open by CFDIFF_1:13, A6;
|.(z1 - z1).| = 0 ;
then z1 in { y where y is Complex : |.(y - z1).| < r / |.a.| } by A7;
then consider W1 being Subset of X such that
A9: ( p in W1 & W1 is open & f .: W1 c= { y where y is Complex : |.(y - z1).| < r / |.a.| } ) by A8, Th3;
set W = W1;
A10: W1 is open by A9;
A11: p in W1 by A9;
(a (#) f) .: W1 c= { y where y is Complex : |.(y - z0).| < r }

proof

let z3 be set ; :: according to TARSKI:def 3 :: thesis: ( not z3 in (a (#) f) .: W1 or z3 in { y where y is Complex : |.(y - z0).| < r } )
assume z3 in (a (#) f) .: W1 ; :: thesis: z3 in { y where y is Complex : |.(y - z0).| < r }
then consider x3 being set such that
A12: ( x3 in dom (a (#) f) & x3 in W1 & (a (#) f) . x3 = z3 ) by FUNCT_1:def 6;
reconsider px = x3 as Point of X by A12;
px in the carrier of X ;
then px in dom f by FUNCT_2:def 1;
then f . px in f .: W1 by A12, FUNCT_1:def 6;
then A14: f . px in { y where y is Complex : |.(y - z1).| < r / |.a.| } by A9;
reconsider a1 = f . px as Complex ;
ex aa1 being Complex st
( f . px = aa1 & |.(aa1 - z1).| < r / |.a.| ) by A14;
then A15: |.(a1 - z1).| < r / |.a.| ;
A16: |.(((a (#) f) . x3) - z0).| = |.((a * (f . px)) - z0).| by A1
.= |.((a * (f . px)) - (a * (f . p))).| by A1
.= |.(a * ((f . px) - (f . p))).|
.= |.a.| * |.(a1 - z1).| by COMPLEX1:65 ;
A17: |.a.| * |.(a1 - z1).| < |.a.| * (r / |.a.|) by A5, A15, XREAL_1:68;
|.a.| * (r / |.a.|) = r * (|.a.| / |.a.|)
.= r * 1 by XCMPLX_1:60, A5
.= r ;
then |.(((a (#) f) . px) - z0).| < r by A16, A17;
hence z3 in { y where y is Complex : |.(y - z0).| < r } by A12; :: thesis: verum

end;

then (a (#) f) .: W1 c= N by A4, XBOOLE_1:1;
hence ex W being Subset of X st
( p in W & W is open & (a (#) f) .: W c= V ) by A10, A11, A3, XBOOLE_1:1; :: thesis: verum

end;

hence a (#) f is continuous by Th3; :: thesis: verum

end;

suppose L2: a = 0 ; :: thesis: a (#) f is continuous

set g = X --> 0c;
set CX = the carrier of X;
A18: dom (X --> 0c) = the carrier of X by FUNCOP_1:13;
dom (a (#) f) = the carrier of X by FUNCT_2:def 1;
then A19: dom (X --> 0c) = dom (a (#) f) by A18;
for z being set st z in dom (a (#) f) holds
(X --> 0c) . z = (a (#) f) . z

proof

let z be set ; :: thesis: ( z in dom (a (#) f) implies (X --> 0c) . z = (a (#) f) . z )
assume A20: z in dom (a (#) f) ; :: thesis: (X --> 0c) . z = (a (#) f) . z
(a (#) f) . z = 0 * (f . z) by L2, VALUED_1:6
.= 0 ;
hence (X --> 0c) . z = (a (#) f) . z by A20, FUNCOP_1:7; :: thesis: verum

end;

hence a (#) f is continuous by A19, FUNCT_1:def 11; :: thesis: verum

end;

end;

end;

hence a (#) f is continuous Function of the carrier of X,COMPLEX ; :: thesis: verum