let X be set ; :: thesis: for S being ZeroStr
for p being Series of X,S
for b being bag of X st b in Support p holds
support b c= vars p
let S be ZeroStr ; :: thesis: for p being Series of X,S
for b being bag of X st b in Support p holds
support b c= vars p
let p be Series of X,S; :: thesis: for b being bag of X st b in Support p holds
support b c= vars p
let b be bag of X; :: thesis: ( b in Support p implies support b c= vars p )
assume A1: b in Support p ; :: thesis: support b c= vars p
set SS = { (support b) where b is Element of Bags X : b in Support p } ;
b in Bags X by PRE_POLY:def 12;
then support b in { (support b) where b is Element of Bags X : b in Support p } by A1;
then support b c= union { (support b) where b is Element of Bags X : b in Support p } by ZFMISC_1:74;
hence support b c= vars p by Th39; :: thesis: verum