let X be Ordinal; :: thesis: for S being non empty right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p, q being Polynomial of X,S holds vars (p *' q) c= (vars p) \/ (vars q)
let S be non empty right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr ; :: thesis: for p, q being Polynomial of X,S holds vars (p *' q) c= (vars p) \/ (vars q)
let p, q be Polynomial of X,S; :: thesis: vars (p *' q) c= (vars p) \/ (vars q)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in vars (p *' q) or x in (vars p) \/ (vars q) )
assume x in vars (p *' q) ; :: thesis: x in (vars p) \/ (vars q)
then consider b being bag of X such that
A1: ( b in Support (p *' q) & b . x <> 0 ) by Def5;
reconsider b = b as Element of Bags X by PRE_POLY:def 12;
consider s being FinSequence of the carrier of S such that
A2: (p *' q) . b = Sum s and
A3: len s = len (decomp b) and
A4: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of X st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by POLYNOM1:def 10;
(p *' q) . b <> 0. S by A1, POLYNOM1:def 4;
then consider k being Nat such that
A5: k in dom s and
A6: s /. k <> 0. S by A2, MATRLIN:11;
consider b1, b2 being bag of X such that
A7: (decomp b) /. k = <*b1,b2*> and
A8: s /. k = (p . b1) * (q . b2) by A4, A5;
A9: b1 in Bags X by PRE_POLY:def 12;
A10: b2 in Bags X by PRE_POLY:def 12;
q . b2 <> 0. S by A6, A8;
then A11: b2 in Support q by A10, POLYNOM1:def 4;
p . b1 <> 0. S by A6, A8;
then A12: b1 in Support p by A9, POLYNOM1:def 4;
k in dom (decomp b) by A3, A5, FINSEQ_3:29;
then consider b19, b29 being bag of X such that
A13: (decomp b) /. k = <*b19,b29*> and
A14: b = b19 + b29 by PRE_POLY:68;
( b19 = b1 & b29 = b2 ) by A7, A13, FINSEQ_1:77;
then b . x = (b1 . x) + (b2 . x) by A14, PRE_POLY:def 5;
then ( b1 . x <> 0 or b2 . x <> 0 ) by A1;
then ( x in vars p or x in vars q ) by A11, A12, Def5;
hence x in (vars p) \/ (vars q) by XBOOLE_0:def 3; :: thesis: verum