let X be non empty TopSpace; :: thesis: for S being LinearTopSpace
for f being Function of X,S
for x being Point of X
for a being Real st f is_continuous_at x holds
a (#) f is_continuous_at x
let S be LinearTopSpace; :: thesis: for f being Function of X,S
for x being Point of X
for a being Real st f is_continuous_at x holds
a (#) f is_continuous_at x
let f be Function of X,S; :: thesis: for x being Point of X
for a being Real st f is_continuous_at x holds
a (#) f is_continuous_at x
let x be Point of X; :: thesis: for a being Real st f is_continuous_at x holds
a (#) f is_continuous_at x
let a be Real; :: thesis: ( f is_continuous_at x implies a (#) f is_continuous_at x )
assume A1: f is_continuous_at x ; :: thesis: a (#) f is_continuous_at x
for G being a_neighborhood of (a (#) f) . x ex H being a_neighborhood of x st (a (#) f) .: H c= G

proof

let G be a_neighborhood of (a (#) f) . x; :: thesis: ex H being a_neighborhood of x st (a (#) f) .: H c= G
A2: dom (a (#) f) = the carrier of X by FUNCT_2:def 1;
A3: (a (#) f) . x = (a (#) f) /. x
.= a * (f /. x) by VFUNCT_1:def 4, A2
.= a * (f . x) ;
consider W being Subset of S such that
A4: ( W is open & W c= G & (a (#) f) . x in W ) by CONNSP_2:6;
consider r being positive Real, W1 being Subset of S such that
A5: ( W1 is open & f . x in W1 & ( for s being Real st |.(s - a).| < r holds
s * W1 c= W ) ) by A3, A4, RLTOPSP1:def 9;
|.(a - a).| = 0 by COMPLEX1:61;
then A6: a * W1 c= W by A5;
reconsider W1 = W1 as a_neighborhood of f . x by A5, CONNSP_2:3;
consider H1 being a_neighborhood of x such that
A7: f .: H1 c= W1 by TMAP_1:def 2, A1;
take H1 ; :: thesis: (a (#) f) .: H1 c= G
thus (a (#) f) .: H1 c= G :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (a (#) f) .: H1 or y in G )
assume y in (a (#) f) .: H1 ; :: thesis: y in G
then consider z being object such that
A8: ( z in the carrier of X & z in H1 & y = (a (#) f) . z ) by FUNCT_2:64;
reconsider z = z as Point of X by A8;
A9: (a (#) f) . z = (a (#) f) /. z
.= a * (f /. z) by VFUNCT_1:def 4, A2
.= a * (f . z) ;
f . z in f .: H1 by FUNCT_2:35, A8;
then a * (f . z) in a * W1 by A7;
hence y in G by A4, A6, A8, A9; :: thesis: verum

end;

end;

hence a (#) f is_continuous_at x by TMAP_1:def 2; :: thesis: verum