let n be Ordinal; :: thesis: for O being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O)))
let O be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O)))
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed left_zeroed doubleLoopStr ; :: thesis: for p, q being non-zero Polynomial of n,L holds (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O)))
let p, q be non-zero Polynomial of n,L; :: thesis: (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O)))
set b = (HT (p,O)) + (HT (q,O));
consider s being FinSequence of L such that
A1: (p *' q) . ((HT (p,O)) + (HT (q,O))) = Sum s and
A2: len s = len (decomp ((HT (p,O)) + (HT (q,O)))) and
A3: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp ((HT (p,O)) + (HT (q,O)))) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by POLYNOM1:def 10;
consider S being non empty finite Subset of (Bags n) such that
A4: divisors ((HT (p,O)) + (HT (q,O))) = SgmX ((BagOrder n),S) and
A5: for p being bag of n holds
( p in S iff p divides (HT (p,O)) + (HT (q,O)) ) by PRE_POLY:def 16;
set sgm = SgmX ((BagOrder n),S);
A6: BagOrder n linearly_orders S by Lm13;
HT (p,O) divides (HT (p,O)) + (HT (q,O)) by PRE_POLY:50;
then HT (p,O) in S by A5;
then HT (p,O) in rng (SgmX ((BagOrder n),S)) by A6, PRE_POLY:def 2;
then consider i being object such that
A7: i in dom (SgmX ((BagOrder n),S)) and
A8: (SgmX ((BagOrder n),S)) . i = HT (p,O) by FUNCT_1:def 3;
A9: i in dom (decomp ((HT (p,O)) + (HT (q,O)))) by A4, A7, PRE_POLY:def 17;
(divisors ((HT (p,O)) + (HT (q,O)))) /. i = HT (p,O) by A4, A7, A8, PARTFUN1:def 6;
then A10: (decomp ((HT (p,O)) + (HT (q,O)))) /. i = <*(HT (p,O)),(((HT (p,O)) + (HT (q,O))) -' (HT (p,O)))*> by A9, PRE_POLY:def 17;
then A11: (decomp ((HT (p,O)) + (HT (q,O)))) /. i = <*(HT (p,O)),(HT (q,O))*> by PRE_POLY:48;
A12: dom s = Seg (len (decomp ((HT (p,O)) + (HT (q,O))))) by A2, FINSEQ_1:def 3
.= dom (decomp ((HT (p,O)) + (HT (q,O)))) by FINSEQ_1:def 3 ;
then A13: i in dom s by A4, A7, PRE_POLY:def 17;
reconsider i = i as Element of NAT by A7;
consider b1, b2 being bag of n such that
A14: (decomp ((HT (p,O)) + (HT (q,O)))) /. i = <*b1,b2*> and
A15: s /. i = (p . b1) * (q . b2) by A3, A13;
A16: b2 = <*(HT (p,O)),(HT (q,O))*> . 2 by A11, A14, FINSEQ_1:44
.= HT (q,O) ;

A17: 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
A18: k in dom s and
A19: k <> i ; :: thesis: s /. k = 0. L
consider b1, b2 being bag of n such that
A20: (decomp ((HT (p,O)) + (HT (q,O)))) /. k = <*b1,b2*> and
A21: s /. k = (p . b1) * (q . b2) by A3, A18;
consider b19, b29 being bag of n such that
A22: (decomp ((HT (p,O)) + (HT (q,O)))) /. k = <*b19,b29*> and
A23: (HT (p,O)) + (HT (q,O)) = b19 + b29 by A12, A18, PRE_POLY:68;
A24: b2 = <*b19,b29*> . 2 by A22, A20, FINSEQ_1:44
.= b29 ;
A25: b1 = <*b19,b29*> . 1 by A22, A20, FINSEQ_1:44
.= b19 ;

A26: now :: thesis: ( p . b1 <> 0. L implies not q . b2 <> 0. L )

assume that
A27: p . b1 <> 0. L and
A28: q . b2 <> 0. L ; :: thesis: contradiction
b1 is Element of Bags n by PRE_POLY:def 12;
then b1 in Support p by A27, POLYNOM1:def 4;
then b1 <= HT (p,O),O by Def6;
then A29: [b1,(HT (p,O))] in O ;
b2 is Element of Bags n by PRE_POLY:def 12;
then b2 in Support q by A28, POLYNOM1:def 4;
then b2 <= HT (q,O),O by Def6;
then A30: [b2,(HT (q,O))] in O ;

A31: now :: thesis: ( b1 = HT (p,O) implies not b2 = HT (q,O) )

assume ( b1 = HT (p,O) & b2 = HT (q,O) ) ; :: thesis: contradiction
then (decomp ((HT (p,O)) + (HT (q,O)))) . k = <*(HT (p,O)),(HT (q,O))*> by A12, A18, A20, PARTFUN1:def 6
.= (decomp ((HT (p,O)) + (HT (q,O)))) /. i by A10, PRE_POLY:48
.= (decomp ((HT (p,O)) + (HT (q,O)))) . i by A9, PARTFUN1:def 6 ;
hence contradiction by A9, A12, A18, A19, FUNCT_1:def 4; :: thesis: verum

end;

now :: thesis: ( ( b1 <> HT (p,O) & contradiction ) or ( b2 <> HT (q,O) & contradiction ) )

per cases ( b1 <> HT (p,O) or b2 <> HT (q,O) ) by A31;

case A32: b1 <> HT (p,O) ; :: thesis: contradiction

A33: now :: thesis: not b1 + b2 = (HT (p,O)) + b2

assume b1 + b2 = (HT (p,O)) + b2 ; :: thesis: contradiction
then b1 = ((HT (p,O)) + b2) -' b2 by PRE_POLY:48;
hence contradiction by A32, PRE_POLY:48; :: thesis: verum

end;

A34: ( (HT (p,O)) + b2 is Element of Bags n & (HT (p,O)) + (HT (q,O)) is Element of Bags n ) by PRE_POLY:def 12;
( [((HT (p,O)) + (HT (q,O))),((HT (p,O)) + b2)] in O & [((HT (p,O)) + b2),((HT (p,O)) + (HT (q,O)))] in O ) by A23, A25, A24, A29, A30, BAGORDER:def 5;
hence contradiction by A23, A25, A24, A33, A34, ORDERS_1:4; :: thesis: verum

end;

case A35: b2 <> HT (q,O) ; :: thesis: contradiction

A36: now :: thesis: not b2 + b1 = (HT (q,O)) + b1

assume b2 + b1 = (HT (q,O)) + b1 ; :: thesis: contradiction
then b2 = ((HT (q,O)) + b1) -' b1 by PRE_POLY:48;
hence contradiction by A35, PRE_POLY:48; :: thesis: verum

end;

A37: ( (HT (q,O)) + b1 is Element of Bags n & (HT (p,O)) + (HT (q,O)) is Element of Bags n ) by PRE_POLY:def 12;
( [((HT (p,O)) + (HT (q,O))),((HT (q,O)) + b1)] in O & [((HT (q,O)) + b1),((HT (p,O)) + (HT (q,O)))] in O ) by A23, A25, A24, A29, A30, BAGORDER:def 5;
hence contradiction by A23, A25, A24, A36, A37, ORDERS_1:4; :: 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 A26;

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 A21; :: thesis: verum

end;

b1 = <*(HT (p,O)),(HT (q,O))*> . 1 by A11, A14, FINSEQ_1:44
.= HT (p,O) ;
hence (p *' q) . ((HT (p,O)) + (HT (q,O))) = (p . (HT (p,O))) * (q . (HT (q,O))) by A1, A13, A17, A15, A16, POLYNOM2:3; :: thesis: verum