let n be Ordinal; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for b being bag of n holds
( b in Support p iff (term m) + b in Support (m *' p) )
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for b being bag of n holds
( b in Support p iff (term m) + b in Support (m *' p) )
let p be Polynomial of n,L; :: thesis: for m being non-zero Monomial of n,L
for b being bag of n holds
( b in Support p iff (term m) + b in Support (m *' p) )
let m be non-zero Monomial of n,L; :: thesis: for b being bag of n holds
( b in Support p iff (term m) + b in Support (m *' p) )
let b be bag of n; :: thesis: ( b in Support p iff (term m) + b in Support (m *' p) )
A1: (m *' p) . ((term m) + b) = (m . (term m)) * (p . b) by POLYRED:7;
m <> 0_ (n,L) by POLYNOM7:def 1;
then Support m <> {} by POLYNOM7:1;
then Support m = {(term m)} by POLYNOM7:7;
then term m in Support m by TARSKI:def 1;
then A2: m . (term m) <> 0. L by POLYNOM1:def 4;

A3: now :: thesis: ( b in Support p implies (term m) + b in Support (m *' p) )

assume b in Support p ; :: thesis: (term m) + b in Support (m *' p)
then p . b <> 0. L by POLYNOM1:def 4;
then ( (term m) + b is Element of Bags n & (m *' p) . ((term m) + b) <> 0. L ) by A2, A1, PRE_POLY:def 12, VECTSP_2:def 1;
hence (term m) + b in Support (m *' p) by POLYNOM1:def 4; :: thesis: verum

end;

now :: thesis: ( (term m) + b in Support (m *' p) implies b in Support p )

assume (term m) + b in Support (m *' p) ; :: thesis: b in Support p
then (m . (term m)) * (p . b) <> 0. L by A1, POLYNOM1:def 4;
then A4: p . b <> 0. L ;
b is Element of Bags n by PRE_POLY:def 12;
hence b in Support p by A4, POLYNOM1:def 4; :: thesis: verum

end;

hence ( b in Support p iff (term m) + b in Support (m *' p) ) by A3; :: thesis: verum