let X be set ; :: thesis: for S being non empty right_zeroed addLoopStr
for p, q being Series of X,S holds vars (p + q) c= (vars p) \/ (vars q)
let S be non empty right_zeroed addLoopStr ; :: thesis: for p, q being Series of X,S holds vars (p + q) c= (vars p) \/ (vars q)
let p, q be Series of X,S; :: thesis: vars (p + q) c= (vars p) \/ (vars q)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in vars (p + q) or x in (vars p) \/ (vars q) )
assume x in vars (p + q) ; :: thesis: x in (vars p) \/ (vars q)
then consider b being bag of X such that
A1: ( b in Support (p + q) & b . x <> 0 ) by Def5;
Support (p + q) c= (Support p) \/ (Support q) by POLYNOM1:20;
then ( b in Support p or b in Support q ) by A1, XBOOLE_0:def 3;
then ( x in vars p or x in vars q ) by A1, Def5;
hence x in (vars p) \/ (vars q) by XBOOLE_0:def 3; :: thesis: verum