let f, g be Function; :: thesis: support (f +* g) c= (support f) \/ (support g)
let a be object ; :: 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 PRE_POLY:def 7;
assume A2: not a in (support f) \/ (support g) ; :: thesis: contradiction
then not a in support f by XBOOLE_0:def 3;
then A3: f . a = 0 by PRE_POLY:def 7;
not a in support g by A2, XBOOLE_0:def 3;
then A4: g . a = 0 by PRE_POLY:def 7;
( a in dom g or not a in dom g ) ;
hence contradiction by A1, A3, A4, FUNCT_4:11, FUNCT_4:13; :: thesis: verum