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 }
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;

A3: now :: thesis: for u being object st u in Support (m *' p) holds
u in { ((term m) + b) where b is Element of Bags n : b in Support p }

let u be object ; :: 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 u9 = u as Element of Bags n ;
u9 in { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support p ) } by A2, A4;
then consider s, t being Element of Bags n such that
A5: ( u9 = s + t & s in Support m ) and
A6: t in Support p ;
u9 = (term m) + t by A1, A5, TARSKI:def 1;
hence u in { ((term m) + b) where b is Element of Bags n : b in Support p } by A6; :: thesis: verum

end;

now :: thesis: for u being object st u in { ((term m) + b) where b is Element of Bags n : b in Support p } holds
u in Support (m *' p)

let u be object ; :: 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 ex t being Element of Bags n st
( u = (term m) + t & t in Support p ) ;
hence u in Support (m *' p) by 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