let n be Ordinal; :: thesis: for L being non trivial domRing-like doubleLoopStr
for p being Polynomial of n,L
for a being non zero Element of L holds Support p c= Support (a * p)
let L be non trivial domRing-like doubleLoopStr ; :: thesis: for p being Polynomial of n,L
for a being non zero Element of L holds Support p c= Support (a * p)
let p be Polynomial of n,L; :: thesis: for a being non zero Element of L holds Support p c= Support (a * p)
let a be non zero Element of L; :: thesis: Support p c= Support (a * p)

now :: thesis: for u being object st u in Support p holds
u in Support (a * p)

let u be object ; :: thesis: ( u in Support p implies u in Support (a * p) )
assume A1: u in Support p ; :: thesis: u in Support (a * p)
then reconsider u9 = u as Element of Bags n ;
A2: ( (a * p) . u9 = a * (p . u9) & a <> 0. L ) by POLYNOM7:def 9;
p . u9 <> 0. L by A1, POLYNOM1:def 4;
then (a * p) . u9 <> 0. L by A2, VECTSP_2:def 1;
hence u in Support (a * p) by POLYNOM1:def 4; :: thesis: verum

end;

hence Support p c= Support (a * p) by TARSKI:def 3; :: thesis: verum