let X be non empty TopSpace; :: thesis: for S being LinearTopSpace
for f being Function of X,S
for a being Real st f is continuous holds
a (#) f is continuous

let S be LinearTopSpace; :: thesis: for f being Function of X,S
for a being Real st f is continuous holds
a (#) f is continuous

let f be Function of X,S; :: thesis: for a being Real st f is continuous holds
a (#) f is continuous

let a be Real; :: thesis: ( f is continuous implies a (#) f is continuous )
assume f is continuous ; :: thesis: a (#) f is continuous
then for x being Point of X holds a (#) f is_continuous_at x by TMAP_1:44, Th2;
hence a (#) f is continuous by TMAP_1:44; :: thesis: verum