let X be non empty TopSpace; :: thesis: for a being Complex
for f being Function of the carrier of X,COMPLEX holds support (a (#) f) c= support f
let a be Complex; :: thesis: for f being Function of the carrier of X,COMPLEX holds support (a (#) f) c= support f
let f be Function of the carrier of X,COMPLEX; :: thesis: support (a (#) f) c= support f
set CX = the carrier of X;
reconsider h = a (#) f as Function of the carrier of X,COMPLEX ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (a (#) f) or 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 a * (f . x) <> 0 by VALUED_1:6;
then f . x <> 0 ;
hence x in support f by PRE_POLY:def 7; :: thesis: verum