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

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