let n be Ordinal; :: thesis: for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L holds Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) }
let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p, q being Polynomial of n,L holds Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) }
let p, q be Polynomial of n,L; :: thesis: Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) }

A1: now

let b be bag of ; :: thesis: ( b in Support (p *' q) implies ex s, t being bag of st
( s in Support p & t in Support q & b = s + t ) )
assume A2: b in Support (p *' q) ; :: thesis: ex s, t being bag of st
( s in Support p & t in Support q & b = s + t )
consider s being FinSequence of L such that
A4: ( (p *' q) . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) by POLYNOM1:def 26;
A5: dom s = Seg (len (decomp b)) by A4, FINSEQ_1:def 3
.= dom (decomp b) by FINSEQ_1:def 3 ;

now

per cases ( dom s = {} or dom s <> {} ) ;

case dom s = {} ; :: thesis: contradiction

then len s = 0 by FINSEQ_1:4, FINSEQ_1:def 3;
then s = <*> the carrier of L ;
hence contradiction by A4; :: thesis: verum

end;

case A6: dom s <> {} ; :: thesis: ex s, t being bag of st
( s in Support p & t in Support q & b = s + t )

consider k being Element of dom s;
k in dom s by A6;
then reconsider k = k as Element of NAT ;

now

assume A7: for k being Element of dom (decomp b)
for b1, b2 being bag of holds
( not (decomp b) /. k = <*b1,b2*> or not p . b1 <> 0. L or not q . b2 <> 0. L ) ; :: thesis: contradiction
A8: for k being Nat st k in dom s holds
s /. k = 0. L

proof

let k be Nat; :: thesis: ( k in dom s implies s /. k = 0. L )
assume A9: k in dom s ; :: thesis: s /. k = 0. L
then consider b1, b2 being bag of such that
A10: ( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by A4;

now

per cases ( p . b1 = 0. L or q . b2 = 0. L ) by A5, A7, A9, A10;

case p . b1 = 0. L ; :: thesis: s /. k = 0. L

hence s /. k = 0. L by A10, BINOM:1; :: thesis: verum

end;

case q . b2 = 0. L ; :: thesis: s /. k = 0. L

hence s /. k = 0. L by A10, BINOM:2; :: thesis: verum

end;

end;

end;

hence s /. k = 0. L ; :: thesis: verum

end;

then for k' being Element of NAT st k' in dom s & k' <> k holds
s /. k' = 0. L ;
then Sum s = s /. k by A6, POLYNOM2:5
.= 0. L by A6, A8 ;
hence contradiction by A2, A4, POLYNOM1:def 9; :: thesis: verum

end;

then consider k being Element of dom (decomp b), b1, b2 being bag of such that
A11: ( (decomp b) /. k = <*b1,b2*> & p . b1 <> 0. L & q . b2 <> 0. L ) ;
k in dom (decomp b) by A5, A6;
then reconsider k = k as Element of NAT ;
( b1 is Element of Bags n & b2 is Element of Bags n ) by POLYNOM1:def 14;
then A12: ( b1 in Support p & b2 in Support q ) by A11, POLYNOM1:def 9;
consider b1', b2' being bag of such that
A13: ( (decomp b) /. k = <*b1',b2'*> & b = b1' + b2' ) by A5, A6, POLYNOM1:72;
A14: b1' = <*b1,b2*> . 1 by A11, A13, FINSEQ_1:61
.= b1 by FINSEQ_1:61 ;
b2' = <*b1,b2*> . 2 by A11, A13, FINSEQ_1:61
.= b2 by FINSEQ_1:61 ;
hence ex s, t being bag of st
( s in Support p & t in Support q & b = s + t ) by A12, A13, A14; :: thesis: verum

end;

end;

end;

hence ex s, t being bag of st
( s in Support p & t in Support q & b = s + t ) ; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in Support (p *' q) implies u in { (s' + t') where s', t' is Element of Bags n : ( s' in Support p & t' in Support q ) } )
assume A15: u in Support (p *' q) ; :: thesis: u in { (s' + t') where s', t' is Element of Bags n : ( s' in Support p & t' in Support q ) }
then reconsider u' = u as Element of Bags n ;
consider s, t being bag of such that
A16: ( s in Support p & t in Support q & u' = s + t ) by A1, A15;
thus u in { (s' + t') where s', t' is Element of Bags n : ( s' in Support p & t' in Support q ) } by A16; :: thesis: verum

end;

hence Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } by TARSKI:def 3; :: thesis: verum