let X be set ; :: thesis: for S being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of X,S holds vars p = vars (- p)
let S be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Series of X,S holds vars p = vars (- p)
let p be Series of X,S; :: thesis: vars p = vars (- p)
thus vars p c= vars (- p) :: according to XBOOLE_0:def 10 :: thesis: vars (- p) c= vars p

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in vars p or x in vars (- p) )
assume x in vars p ; :: thesis: x in vars (- p)
then consider b being bag of X such that
A1: ( b in Support p & b . x <> 0 ) by Def5;
reconsider b = b as Element of Bags X by PRE_POLY:def 12;
( - (p . b) <> - (0. S) & - (0. S) = 0. S ) by A1, POLYNOM1:def 4;
then (- p) . b <> 0. S by POLYNOM1:17;
then b in Support (- p) by POLYNOM1:def 4;
hence x in vars (- p) by A1, Def5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in vars (- p) or x in vars p )
assume x in vars (- p) ; :: thesis: x in vars p
then consider b being bag of X such that
A2: ( b in Support (- p) & b . x <> 0 ) by Def5;
reconsider b = b as Element of Bags X by PRE_POLY:def 12;
( - ((- p) . b) <> - (0. S) & - (0. S) = 0. S ) by A2, POLYNOM1:def 4;
then (- (- p)) . b <> 0. S by POLYNOM1:17;
then b in Support (- (- p)) by POLYNOM1:def 4;
then b in Support p by POLYNOM1:19;
hence x in vars p by A2, Def5; :: thesis: verum