consider b11 being bag of n such that
A1: ( p . b11 <> 0. L & ( for b' being bag of n st b11 < b' holds
p . b' = 0. L ) ) by Lm5;
consider b22 being bag of n such that
A2: ( q . b22 <> 0. L & ( for b' being bag of n st b22 < b' holds
q . b' = 0. L ) ) by Lm5;
set b = b11 + b22;
consider s being FinSequence of the carrier of L such that
A3: ( (p *' q) . (b11 + b22) = Sum s & len s = len (decomp (b11 + b22)) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp (b11 + b22)) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) by POLYNOM1:def 26;
consider S being non empty finite Subset of (Bags n) such that
A4: ( divisors (b11 + b22) = SgmX (BagOrder n),S & ( for p being bag of n holds
( p in S iff p divides b11 + b22 ) ) ) by POLYNOM1:def 18;
b11 divides b11 + b22 by POLYNOM1:54;
then A5: b11 in S by A4;
set sgm = SgmX (BagOrder n),S;
BagOrder n linearly_orders S by Lm1;
then b11 in rng (SgmX (BagOrder n),S) by A5, TRIANG_1:def 2;
then consider i being set such that
A6: ( i in dom (SgmX (BagOrder n),S) & (SgmX (BagOrder n),S) . i = b11 ) by FUNCT_1:def 5;
A7: i in dom (decomp (b11 + b22)) by A4, A6, POLYNOM1:def 19;
(divisors (b11 + b22)) /. i = b11 by A4, A6, PARTFUN1:def 8;
then A8: (decomp (b11 + b22)) /. i = <*b11,((b11 + b22) -' b11)*> by A7, POLYNOM1:def 19;
then A9: (decomp (b11 + b22)) /. i = <*b11,b22*> by POLYNOM1:52;
A10: dom s = Seg (len (decomp (b11 + b22))) by A3, FINSEQ_1:def 3
.= dom (decomp (b11 + b22)) by FINSEQ_1:def 3 ;
then A11: i in dom s by A4, A6, POLYNOM1:def 19;
reconsider i = i as Element of NAT by A6;

A12: now

let k be Element of NAT ; :: thesis: ( k in dom s & k <> i implies s /. k = 0. L )
assume A13: ( k in dom s & k <> i ) ; :: thesis: s /. k = 0. L
then consider b1', b2' being bag of n such that
A14: ( (decomp (b11 + b22)) /. k = <*b1',b2'*> & b11 + b22 = b1' + b2' ) by A10, POLYNOM1:72;
consider b1, b2 being bag of n such that
A15: ( (decomp (b11 + b22)) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by A3, A13;
A16: b1 = <*b1',b2'*> . 1 by A14, A15, FINSEQ_1:61
.= b1' by FINSEQ_1:61 ;
A17: b2 = <*b1',b2'*> . 2 by A14, A15, FINSEQ_1:61
.= b2' by FINSEQ_1:61 ;

A18: now

assume ( p . b1 <> 0. L & q . b2 <> 0. L ) ; :: thesis: contradiction
then ( not b11 < b1 & not b22 < b2 ) by A1, A2;
then A19: ( b1 <=' b11 & b2 <=' b22 ) by Lm4;

A20: now

assume ( b1 = b11 & b2 = b22 ) ; :: thesis: contradiction
then (decomp (b11 + b22)) . k = <*b11,b22*> by A10, A13, A15, PARTFUN1:def 8
.= (decomp (b11 + b22)) /. i by A8, POLYNOM1:52
.= (decomp (b11 + b22)) . i by A7, PARTFUN1:def 8 ;
hence contradiction by A7, A10, A13, FUNCT_1:def 8; :: thesis: verum

end;

now

per cases ( b1 <> b11 or b2 <> b22 ) by A20;

case A21: b1 <> b11 ; :: thesis: contradiction

A22: now

assume b1 + b2 = b11 + b2 ; :: thesis: contradiction
then b1 = (b11 + b2) -' b2 by POLYNOM1:52;
hence contradiction by A21, POLYNOM1:52; :: thesis: verum

end;

A23: b11 + b22 <=' b11 + b2 by A14, A16, A17, A19, Lm2;
b11 + b2 <=' b11 + b22 by A19, Lm2;
hence contradiction by A14, A16, A17, A22, A23, Lm3; :: thesis: verum

end;

case A24: b2 <> b22 ; :: thesis: contradiction

A25: now

assume b2 + b1 = b22 + b1 ; :: thesis: contradiction
then b2 = (b22 + b1) -' b1 by POLYNOM1:52;
hence contradiction by A24, POLYNOM1:52; :: thesis: verum

end;

A26: b11 + b22 <=' b22 + b1 by A14, A16, A17, A19, Lm2;
b22 + b1 <=' b11 + b22 by A19, Lm2;
hence contradiction by A14, A16, A17, A25, A26, Lm3; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

now

per cases ( p . b1 = 0. L or q . b2 = 0. L ) by A18;

case p . b1 = 0. L ; :: thesis: (p . b1) * (q . b2) = 0. L

hence (p . b1) * (q . b2) = 0. L by BINOM:1; :: thesis: verum

end;

case q . b2 = 0. L ; :: thesis: (p . b1) * (q . b2) = 0. L

hence (p . b1) * (q . b2) = 0. L by BINOM:2; :: thesis: verum

end;

end;

end;

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

end;

consider b1, b2 being bag of n such that
A27: ( (decomp (b11 + b22)) /. i = <*b1,b2*> & s /. i = (p . b1) * (q . b2) ) by A3, A11;
A28: b1 = <*b11,b22*> . 1 by A9, A27, FINSEQ_1:61
.= b11 by FINSEQ_1:61 ;
b2 = <*b11,b22*> . 2 by A9, A27, FINSEQ_1:61
.= b22 by FINSEQ_1:61 ;
then A29: (p *' q) . (b11 + b22) = (p . b11) * (q . b22) by A3, A11, A12, A27, A28, POLYNOM2:5;
A30: b11 + b22 is Element of Bags n by POLYNOM1:def 14;
(p . b11) * (q . b22) <> 0. L by A1, A2, VECTSP_2:def 5;
then b11 + b22 in Support (p *' q) by A29, A30, POLYNOM1:def 9;
then p *' q <> 0_ n,L by POLYNOM7:1;
hence p *' q is non-zero by POLYNOM7:def 2; :: thesis: verum