let X be non empty TopSpace; :: thesis: for a being Complex
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; :: 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 :: thesis: a (#) f is continuous

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

suppose A2: 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 A3: ( (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
A4: N c= V by A3, CFDIFF_1:9;
consider r being Real such that
A5: ( 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 } ;
A6: |.a.| > 0 by A2;
A7: r / |.a.| > 0 by A2, A5;
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 object ; :: 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 by XCMPLX_0:def 2; :: 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;
|.(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 object ; :: 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 object 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 A13: 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 A13;
then A14: |.(a1 - z1).| < r / |.a.| ;
A15: |.(((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 ;
A16: |.a.| * |.(a1 - z1).| < |.a.| * (r / |.a.|) by A6, A14, XREAL_1:68;
|.a.| * (r / |.a.|) = r * (|.a.| / |.a.|)
.= r * 1 by A6, XCMPLX_1:60
.= r ;
then |.(((a (#) f) . px) - z0).| < r by A15, A16;
hence z3 in { y where y is Complex : |.(y - z0).| < r } by A12; :: thesis: verum

end;

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

end;

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

end;

suppose A17: 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 object st z in dom (a (#) f) holds
(X --> 0c) . z = (a (#) f) . z

proof

let z be object ; :: 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 A17, 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