let n be Ordinal; :: thesis: for L being non empty ZeroStr
for p being Polynomial of n,L
for b being bag of n holds Support (b *' p) c= { (b + b9) where b9 is Element of Bags n : b9 in Support p }
let L be non empty ZeroStr ; :: thesis: for p being Polynomial of n,L
for b being bag of n holds Support (b *' p) c= { (b + b9) where b9 is Element of Bags n : b9 in Support p }
let p be Polynomial of n,L; :: thesis: for b being bag of n holds Support (b *' p) c= { (b + b9) where b9 is Element of Bags n : b9 in Support p }
let b be bag of n; :: thesis: Support (b *' p) c= { (b + b9) where b9 is Element of Bags n : b9 in Support p }
now :: thesis: for u being object st u in Support (b *' p) holds
u in { (b + b9) where b9 is Element of Bags n : b9 in Support p }
let u be object ; :: thesis: ( u in Support (b *' p) implies u in { (b + b9) where b9 is Element of Bags n : b9 in Support p } )
assume A1: u in Support (b *' p) ; :: thesis: u in { (b + b9) where b9 is Element of Bags n : b9 in Support p }
then reconsider u9 = u as Element of Bags n ;
A2: (b *' p) . u9 <> 0. L by A1, POLYNOM1:def 4;
then b divides u9 by Def1;
then consider s being bag of n such that
A3: u9 = b + s by TERMORD:1;
( s is Element of Bags n & p . s <> 0. L ) by A2, A3, Lm9, PRE_POLY:def 12;
then s in Support p by POLYNOM1:def 4;
hence u in { (b + b9) where b9 is Element of Bags n : b9 in Support p } by A3; :: thesis: verum
end;
hence Support (b *' p) c= { (b + b9) where b9 is Element of Bags n : b9 in Support p } by TARSKI:def 3; :: thesis: verum