let f, g be complex-valued Function; :: thesis: support (f (#) g) c= support f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (f (#) g) or x in support f )
assume A1: x in support (f (#) g) ; :: thesis: x in support f
(f (#) g) . x = (f . x) * (g . x) by VALUED_1:5;
then f . x <> 0 by A1, PRE_POLY:def 7;
hence x in support f by PRE_POLY:def 7; :: thesis: verum