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