let X be set ; :: thesis: for S being ZeroStr
for p being Series of X,S holds vars p = union { (support b) where b is Element of Bags X : b in Support p }
let S be ZeroStr ; :: thesis: for p being Series of X,S holds vars p = union { (support b) where b is Element of Bags X : b in Support p }
let p be Series of X,S; :: thesis: vars p = union { (support b) where b is Element of Bags X : b in Support p }
set F = { (support b) where b is Element of Bags X : b in Support p } ;
thus vars p c= union { (support b) where b is Element of Bags X : b in Support p } :: according to XBOOLE_0:def 10 :: thesis: union { (support b) where b is Element of Bags X : b in Support p } c= vars p

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in vars p or x in union { (support b) where b is Element of Bags X : b in Support p } )
assume x in vars p ; :: thesis: x in union { (support b) where b is Element of Bags X : b in Support p }
then consider b being bag of X such that
A1: ( b in Support p & b . x <> 0 ) by Def5;
b in Bags X by PRE_POLY:def 12;
then ( x in support b & support b in { (support b) where b is Element of Bags X : b in Support p } ) by A1, PRE_POLY:def 7;
hence x in union { (support b) where b is Element of Bags X : b in Support p } by TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (support b) where b is Element of Bags X : b in Support p } or x in vars p )
assume x in union { (support b) where b is Element of Bags X : b in Support p } ; :: thesis: x in vars p
then consider B being set such that
A2: ( x in B & B in { (support b) where b is Element of Bags X : b in Support p } ) by TARSKI:def 4;
consider b being Element of Bags X such that
A3: ( B = support b & b in Support p ) by A2;
b . x <> 0 by A2, A3, PRE_POLY:def 7;
hence x in vars p by A3, Def5; :: thesis: verum