let X be non empty TopSpace; :: thesis: for T being RealLinearSpace
for f being Function of X,T
for a being Real holds support (a (#) f) c= support f
let T be RealLinearSpace; :: thesis: for f being Function of X,T
for a being Real holds support (a (#) f) c= support f
let f be Function of X,T; :: thesis: for a being Real holds support (a (#) f) c= support f
let a be Real; :: thesis: support (a (#) f) c= support f
set CX = the carrier of X;
reconsider h = a (#) f as Function of X,T ;

now :: thesis: for x being object st x in support (a (#) f) holds
x in support f

let x be object ; :: thesis: ( x in support (a (#) f) implies x in support f )
assume x in support (a (#) f) ; :: thesis: x in support f
then A1: ( x in dom (a (#) f) & (a (#) f) /. x <> 0. T ) by Def10;
then a * (f /. x) <> 0. T by VFUNCT_1:def 4;
then A3: f /. x <> 0. T ;
x in dom f by A1, VFUNCT_1:def 4;
hence x in support f by A3, Def10; :: thesis: verum

end;

hence support (a (#) f) c= support f ; :: thesis: verum