let f, g be Function; :: thesis: support (f +* g) c= (support f) \/ (support g)
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in support (f +* g) or a in (support f) \/ (support g) )
assume a in support (f +* g) ; :: thesis: a in (support f) \/ (support g)
then A1: (f +* g) . a <> 0 by POLYNOM1:def 7;
assume not a in (support f) \/ (support g) ; :: thesis: contradiction
then ( not a in support f & not a in support g ) by XBOOLE_0:def 3;
then A2: ( f . a = 0 & g . a = 0 ) by POLYNOM1:def 7;
( a in dom g or not a in dom g ) ;
hence contradiction by A1, A2, FUNCT_4:12, FUNCT_4:14; :: thesis: verum