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

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 (a (#) f) . x <> 0 by PRE_POLY:def 7;
then A1: a * (f . x) <> 0 by VALUED_1:6;
f . x <> 0 by A1;
hence x in support f by PRE_POLY:def 7; :: thesis: verum

end;

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