let n be Ordinal; :: thesis: for L being non empty ZeroStr
for p being Polynomial of n,L
for b being bag of holds Support (b *' p) c= { (b + b') where b' is Element of Bags n : b' in Support p }
let L be non empty ZeroStr ; :: thesis: for p being Polynomial of n,L
for b being bag of holds Support (b *' p) c= { (b + b') where b' is Element of Bags n : b' in Support p }
let p be Polynomial of n,L; :: thesis: for b being bag of holds Support (b *' p) c= { (b + b') where b' is Element of Bags n : b' in Support p }
let b be bag of ; :: thesis: Support (b *' p) c= { (b + b') where b' is Element of Bags n : b' in Support p }

now

let u be set ; :: thesis: ( u in Support (b *' p) implies u in { (b + b') where b' is Element of Bags n : b' in Support p } )
assume A1: u in Support (b *' p) ; :: thesis: u in { (b + b') where b' is Element of Bags n : b' in Support p }
then reconsider u' = u as Element of Bags n ;
A2: (b *' p) . u' <> 0. L by A1, POLYNOM1:def 9;
then b divides u' by Def1;
then consider s being bag of such that
A3: u' = b + s by TERMORD:1;
A4: s is Element of Bags n by POLYNOM1:def 14;
p . s <> 0. L by A2, A3, Lm9;
then s in Support p by A4, POLYNOM1:def 9;
hence u in { (b + b') where b' is Element of Bags n : b' in Support p } by A3; :: thesis: verum

end;

hence Support (b *' p) c= { (b + b') where b' is Element of Bags n : b' in Support p } by TARSKI:def 3; :: thesis: verum