consider b22 being bag of n such that
A1: q . b22 <> 0. L and
A2: for b9 being bag of n st b22 < b9 holds
q . b9 = 0. L by Lm5;
consider b11 being bag of n such that
A3: p . b11 <> 0. L and
A4: for b9 being bag of n st b11 < b9 holds
p . b9 = 0. L by Lm5;
set b = b11 + b22;
consider s being FinSequence of the carrier of L such that
A5: (p *' q) . (b11 + b22) = Sum s and
A6: len s = len (decomp (b11 + b22)) and
A7: 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 10;
A8: ( b11 + b22 is Element of Bags n & (p . b11) * (q . b22) <> 0. L ) by A3, A1, PRE_POLY:def 12, VECTSP_2:def 1;
consider S being non empty finite Subset of (Bags n) such that
A9: divisors (b11 + b22) = SgmX ((BagOrder n),S) and
A10: for p being bag of n holds
( p in S iff p divides b11 + b22 ) by PRE_POLY:def 16;
set sgm = SgmX ((BagOrder n),S);
A11: BagOrder n linearly_orders S by Lm1;
b11 divides b11 + b22 by PRE_POLY:50;
then b11 in S by A10;
then b11 in rng (SgmX ((BagOrder n),S)) by A11, PRE_POLY:def 2;
then consider i being object such that
A12: i in dom (SgmX ((BagOrder n),S)) and
A13: (SgmX ((BagOrder n),S)) . i = b11 by FUNCT_1:def 3;
A14: i in dom (decomp (b11 + b22)) by A9, A12, PRE_POLY:def 17;
(divisors (b11 + b22)) /. i = b11 by A9, A12, A13, PARTFUN1:def 6;
then A15: (decomp (b11 + b22)) /. i = <*b11,((b11 + b22) -' b11)*> by A14, PRE_POLY:def 17;
then A16: (decomp (b11 + b22)) /. i = <*b11,b22*> by PRE_POLY:48;
A17: dom s = Seg (len (decomp (b11 + b22))) by A6, FINSEQ_1:def 3
.= dom (decomp (b11 + b22)) by FINSEQ_1:def 3 ;
then A18: i in dom s by A9, A12, PRE_POLY:def 17;
reconsider i = i as Element of NAT by A12;
consider b1, b2 being bag of n such that
A19: (decomp (b11 + b22)) /. i = <*b1,b2*> and
A20: s /. i = (p . b1) * (q . b2) by A7, A18;
A21: b2 = <*b11,b22*> . 2 by A16, A19, FINSEQ_1:44
.= b22 by FINSEQ_1:44 ;
A22: now :: thesis: for k being Element of NAT st k in dom s & k <> i holds
s /. k = 0. L
let k be Element of NAT ; :: thesis: ( k in dom s & k <> i implies s /. k = 0. L )
assume that
A23: k in dom s and
A24: k <> i ; :: thesis: s /. k = 0. L
consider b1, b2 being bag of n such that
A25: (decomp (b11 + b22)) /. k = <*b1,b2*> and
A26: s /. k = (p . b1) * (q . b2) by A7, A23;
consider b19, b29 being bag of n such that
A27: (decomp (b11 + b22)) /. k = <*b19,b29*> and
A28: b11 + b22 = b19 + b29 by A17, A23, PRE_POLY:68;
A29: b2 = <*b19,b29*> . 2 by A27, A25, FINSEQ_1:44
.= b29 by FINSEQ_1:44 ;
A30: b1 = <*b19,b29*> . 1 by A27, A25, FINSEQ_1:44
.= b19 by FINSEQ_1:44 ;
A31: now :: thesis: ( p . b1 <> 0. L implies not q . b2 <> 0. L )
assume that
A32: p . b1 <> 0. L and
A33: q . b2 <> 0. L ; :: thesis: contradiction
not b11 < b1 by A4, A32;
then A34: b1 <=' b11 by Lm4;
not b22 < b2 by A2, A33;
then A35: b2 <=' b22 by Lm4;
A36: now :: thesis: ( b1 = b11 implies not b2 = b22 )
assume ( b1 = b11 & b2 = b22 ) ; :: thesis: contradiction
then (decomp (b11 + b22)) . k = <*b11,b22*> by A17, A23, A25, PARTFUN1:def 6
.= (decomp (b11 + b22)) /. i by A15, PRE_POLY:48
.= (decomp (b11 + b22)) . i by A14, PARTFUN1:def 6 ;
hence contradiction by A14, A17, A23, A24, FUNCT_1:def 4; :: thesis: verum
end;
now :: thesis: ( ( b1 <> b11 & contradiction ) or ( b2 <> b22 & contradiction ) )
per cases ( b1 <> b11 or b2 <> b22 ) by A36;
case A37: b1 <> b11 ; :: thesis: contradiction
A38: now :: thesis: not b1 + b2 = b11 + b2
assume b1 + b2 = b11 + b2 ; :: thesis: contradiction
then b1 = (b11 + b2) -' b2 by PRE_POLY:48;
hence contradiction by A37, PRE_POLY:48; :: thesis: verum
end;
( b11 + b22 <=' b11 + b2 & b11 + b2 <=' b11 + b22 ) by A28, A30, A29, A34, A35, Lm2;
hence contradiction by A28, A30, A29, A38, Lm3; :: thesis: verum
end;
case A39: b2 <> b22 ; :: thesis: contradiction
A40: now :: thesis: not b2 + b1 = b22 + b1
assume b2 + b1 = b22 + b1 ; :: thesis: contradiction
then b2 = (b22 + b1) -' b1 by PRE_POLY:48;
hence contradiction by A39, PRE_POLY:48; :: thesis: verum
end;
( b11 + b22 <=' b22 + b1 & b22 + b1 <=' b11 + b22 ) by A28, A30, A29, A34, A35, Lm2;
hence contradiction by A28, A30, A29, A40, Lm3; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
now :: thesis: ( ( p . b1 = 0. L & (p . b1) * (q . b2) = 0. L ) or ( q . b2 = 0. L & (p . b1) * (q . b2) = 0. L ) )
per cases ( p . b1 = 0. L or q . b2 = 0. L ) by A31;
case p . b1 = 0. L ; :: thesis: (p . b1) * (q . b2) = 0. L
hence (p . b1) * (q . b2) = 0. L ; :: thesis: verum
end;
case q . b2 = 0. L ; :: thesis: (p . b1) * (q . b2) = 0. L
hence (p . b1) * (q . b2) = 0. L ; :: thesis: verum
end;
end;
end;
hence s /. k = 0. L by A26; :: thesis: verum
end;
b1 = <*b11,b22*> . 1 by A16, A19, FINSEQ_1:44
.= b11 by FINSEQ_1:44 ;
then (p *' q) . (b11 + b22) = (p . b11) * (q . b22) by A5, A18, A22, A20, A21, POLYNOM2:3;
then b11 + b22 in Support (p *' q) by A8, POLYNOM1:def 4;
then p *' q <> 0_ (n,L) by POLYNOM7:1;
hence p *' q is non-zero ; :: thesis: verum