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 :: thesis: for b being bag of n st b in Support (p *' q) holds
ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t )

let b be bag of n; :: thesis: ( b in Support (p *' q) implies ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t ) )
consider s being FinSequence of L 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 n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by POLYNOM1:def 10;
A5: dom s = Seg (len (decomp b)) by A3, FINSEQ_1:def 3
.= dom (decomp b) by FINSEQ_1:def 3 ;
assume A6: b in Support (p *' q) ; :: thesis: ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t )

now :: thesis: ( ( dom s = {} & contradiction ) or ( dom s <> {} & ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t ) ) )

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

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

then Seg (len s) = {} by FINSEQ_1:def 3;
then len s = 0 ;
hence contradiction by A3; :: thesis: verum

end;

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

set k = the Element of dom s;
the Element of dom s in dom s by A7;
then reconsider k = the Element of dom s as Element of NAT ;

now :: thesis: ex k being Element of dom (decomp b) ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & p . b1 <> 0. L & q . b2 <> 0. L )

assume A8: for k being Element of dom (decomp b)
for b1, b2 being bag of n holds
( not (decomp b) /. k = <*b1,b2*> or not p . b1 <> 0. L or not q . b2 <> 0. L ) ; :: thesis: contradiction
A9: 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 A10: k in dom s ; :: thesis: s /. k = 0. L
then consider b1, b2 being bag of n such that
A11: (decomp b) /. k = <*b1,b2*> and
A12: s /. k = (p . b1) * (q . b2) by A4;

now :: thesis: ( ( p . b1 = 0. L & s /. k = 0. L ) or ( q . b2 = 0. L & s /. k = 0. L ) )

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

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

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

end;

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

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

end;

end;

end;

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

end;

then for k9 being Element of NAT st k9 in dom s & k9 <> k holds
s /. k9 = 0. L ;
then Sum s = s /. k by A7, POLYNOM2:3
.= 0. L by A7, A9 ;
hence contradiction by A6, A2, POLYNOM1:def 4; :: thesis: verum

end;

then consider k being Element of dom (decomp b), b1, b2 being bag of n such that
A13: (decomp b) /. k = <*b1,b2*> and
A14: p . b1 <> 0. L and
A15: q . b2 <> 0. L ;
k in dom (decomp b) by A5, A7;
then reconsider k = k as Element of NAT ;
consider b19, b29 being bag of n such that
A16: (decomp b) /. k = <*b19,b29*> and
A17: b = b19 + b29 by A5, A7, PRE_POLY:68;
A18: b29 = <*b1,b2*> . 2 by A13, A16, FINSEQ_1:44
.= b2 ;
b2 is Element of Bags n by PRE_POLY:def 12;
then A19: b2 in Support q by A15, POLYNOM1:def 4;
b1 is Element of Bags n by PRE_POLY:def 12;
then A20: b1 in Support p by A14, POLYNOM1:def 4;
b19 = <*b1,b2*> . 1 by A13, A16, FINSEQ_1:44
.= b1 ;
hence ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t ) by A20, A19, A17, A18; :: thesis: verum

end;

end;

end;

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

end;

now :: thesis: for u being object st u in Support (p *' q) holds
u in { (s9 + t9) where s9, t9 is Element of Bags n : ( s9 in Support p & t9 in Support q ) }

let u be object ; :: thesis: ( u in Support (p *' q) implies u in { (s9 + t9) where s9, t9 is Element of Bags n : ( s9 in Support p & t9 in Support q ) } )
assume A21: u in Support (p *' q) ; :: thesis: u in { (s9 + t9) where s9, t9 is Element of Bags n : ( s9 in Support p & t9 in Support q ) }
then reconsider u9 = u as Element of Bags n ;
ex s, t being bag of n st
( s in Support p & t in Support q & u9 = s + t ) by A1, A21;
hence u in { (s9 + t9) where s9, t9 is Element of Bags n : ( s9 in Support p & t9 in Support q ) } ; :: 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 ) } ; :: thesis: verum