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 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 ; :: thesis: 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; :: thesis: 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; :: thesis: Support (m *' p) = { ((term m) + b) where b is Element of Bags n : b in Support p }
A1: 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;
m <> 0_ n,L by POLYNOM7:def 2;
then Support m <> {} by POLYNOM7:1;
then A2: Support m = {(term m)} by POLYNOM7:7;

A3: now

let u be set ; :: thesis: ( u in Support (m *' p) implies u in { ((term m) + b) where b is Element of Bags n : b in Support p } )
assume A4: u in Support (m *' p) ; :: thesis: u in { ((term m) + b) where b is Element of Bags n : b in Support p }
then reconsider u' = u as Element of Bags n ;
u' in { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support p ) } by A1, A4;
then consider s, t being Element of Bags n such that
A5: ( u' = s + t & s in Support m & t in Support p ) ;
u' = (term m) + t by A2, A5, TARSKI:def 1;
hence u in { ((term m) + b) where b is Element of Bags n : b in Support p } by A5; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in { ((term m) + b) where b is Element of Bags n : b in Support p } implies u in Support (m *' p) )
assume u in { ((term m) + b) where b is Element of Bags n : b in Support p } ; :: thesis: u in Support (m *' p)
then consider t being Element of Bags n such that
A6: ( u = (term m) + t & t in Support p ) ;
thus u in Support (m *' p) by A6, Th8; :: thesis: verum

end;

hence Support (m *' p) = { ((term m) + b) where b is Element of Bags n : b in Support p } by A3, TARSKI:2; :: thesis: verum