let n be Ordinal; 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 holds Support (m *' p) = { ((term m) + b) where b is Element of Bags n : b in Support p }
let L be 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 holds Support (m *' p) = { ((term m) + b) where b is Element of Bags n : b in Support p }
let p be Polynomial of n,L; for m being non-zero Monomial of n,L holds Support (m *' p) = { ((term m) + b) where b is Element of Bags n : b in Support p }
let m be non-zero Monomial of n,L; Support (m *' p) = { ((term m) + b) where b is Element of Bags n : b in Support p }
m <> 0_ (n,L)
by POLYNOM7:def 1;
then
Support m <> {}
by POLYNOM7:1;
then A1:
Support m = {(term m)}
by POLYNOM7:7;
A2:
Support (m *' p) c= { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support p ) }
by TERMORD:30;
hence
Support (m *' p) = { ((term m) + b) where b is Element of Bags n : b in Support p }
by A3, TARSKI:2; verum