let n be set ; :: thesis: for L being non empty right_zeroed addLoopStr
for p, q being Series of n,L holds Support (p + q) c= (Support p) \/ (Support q)
let L be non empty right_zeroed addLoopStr ; :: thesis: for p, q being Series of n,L holds Support (p + q) c= (Support p) \/ (Support q)
let p, q be Series of n,L; :: thesis: Support (p + q) c= (Support p) \/ (Support q)
set f = p + q;
set Sp = Support p;
set Sq = Support q;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support (p + q) or x in (Support p) \/ (Support q) )
assume A1: x in Support (p + q) ; :: thesis: x in (Support p) \/ (Support q)
then reconsider x9 = x as Element of Bags n ;
(p + q) . x9 <> 0. L by A1, Def4;
then (p . x9) + (q . x9) <> 0. L by Th15;
then ( not p . x9 = 0. L or not q . x9 = 0. L ) by RLVECT_1:def 4;
then ( x9 in Support p or x9 in Support q ) by Def4;
hence x in (Support p) \/ (Support q) by XBOOLE_0:def 3; :: thesis: verum