let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of n,L
for b1, b2 being bag of st Support p = {b1} & Support q = {b2} holds
for x being Function of n,L holds eval (p *' q),x = (eval p,x) * (eval q,x)
let L be non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p, q being Polynomial of n,L
for b1, b2 being bag of st Support p = {b1} & Support q = {b2} holds
for x being Function of n,L holds eval (p *' q),x = (eval p,x) * (eval q,x)
let p, q be Polynomial of n,L; :: thesis: for b1, b2 being bag of st Support p = {b1} & Support q = {b2} holds
for x being Function of n,L holds eval (p *' q),x = (eval p,x) * (eval q,x)
let b1, b2 be bag of ; :: thesis: ( Support p = {b1} & Support q = {b2} implies for x being Function of n,L holds eval (p *' q),x = (eval p,x) * (eval q,x) )
assume A1: ( Support p = {b1} & Support q = {b2} ) ; :: thesis: for x being Function of n,L holds eval (p *' q),x = (eval p,x) * (eval q,x)
let x be Function of n,L; :: thesis: eval (p *' q),x = (eval p,x) * (eval q,x)
A2: for b being bag of st b <> b1 holds
p . b = 0. L

proof

let b be bag of ; :: thesis: ( b <> b1 implies p . b = 0. L )
assume b <> b1 ; :: thesis: p . b = 0. L
then A3: not b in Support p by A1, TARSKI:def 1;
b is Element of Bags n by POLYNOM1:def 14;
hence p . b = 0. L by A3, POLYNOM1:def 9; :: thesis: verum

end;

A4: for b being bag of st b <> b2 holds
q . b = 0. L

proof

let b be bag of ; :: thesis: ( b <> b2 implies q . b = 0. L )
assume b <> b2 ; :: thesis: q . b = 0. L
then A5: not b in Support q by A1, TARSKI:def 1;
b is Element of Bags n by POLYNOM1:def 14;
hence q . b = 0. L by A5, POLYNOM1:def 9; :: thesis: verum

end;

consider s being FinSequence of the carrier of L such that
A6: ( (p *' q) . (b1 + b2) = Sum s & len s = len (decomp (b1 + b2)) & ( for k being Element of NAT st k in dom s holds
ex u1, u2 being bag of st
( (decomp (b1 + b2)) /. k = <*u1,u2*> & s /. k = (p . u1) * (q . u2) ) ) ) by POLYNOM1:def 26;
A7: dom s = Seg (len s) by FINSEQ_1:def 3
.= dom (decomp (b1 + b2)) by A6, FINSEQ_1:def 3 ;
consider k being Element of NAT such that
A8: ( k in dom (decomp (b1 + b2)) & (decomp (b1 + b2)) /. k = <*b1,b2*> ) by POLYNOM1:73;
consider b1', b2' being bag of such that
A9: ( (decomp (b1 + b2)) /. k = <*b1',b2'*> & s /. k = (p . b1') * (q . b2') ) by A6, A7, A8;
A10: b1 = <*b1',b2'*> . 1 by A8, A9, FINSEQ_1:61
.= b1' by FINSEQ_1:61 ;
A11: b2 = <*b1,b2*> . 2 by FINSEQ_1:61
.= b2' by A8, A9, FINSEQ_1:61 ;
for k' being Element of NAT st k' in dom s & k' <> k holds
s /. k' = 0. L

proof

let k' be Element of NAT ; :: thesis: ( k' in dom s & k' <> k implies s /. k' = 0. L )
assume A12: ( k' in dom s & k' <> k ) ; :: thesis: s /. k' = 0. L
then consider b1', b2' being bag of such that
A13: ( (decomp (b1 + b2)) /. k' = <*b1',b2'*> & s /. k' = (p . b1') * (q . b2') ) by A6;

per cases ( ( b1' = b1 & b2' = b2 ) or b1' <> b1 or b2' <> b2 ) ;

suppose A14: ( b1' = b1 & b2' = b2 ) ; :: thesis: s /. k' = 0. L

(decomp (b1 + b2)) . k' = (decomp (b1 + b2)) /. k' by A7, A12, PARTFUN1:def 8
.= (decomp (b1 + b2)) . k by A8, A13, A14, PARTFUN1:def 8 ;
hence s /. k' = 0. L by A7, A8, A12, FUNCT_1:def 8; :: thesis: verum

end;

suppose b1' <> b1 ; :: thesis: s /. k' = 0. L

then p . b1' = 0. L by A2;
hence s /. k' = 0. L by A13, VECTSP_1:39; :: thesis: verum

end;

suppose b2' <> b2 ; :: thesis: s /. k' = 0. L

then q . b2' = 0. L by A4;
hence s /. k' = 0. L by A13, VECTSP_1:39; :: thesis: verum

end;

end;

end;

then A15: (p *' q) . (b1 + b2) = (p . b1) * (q . b2) by A6, A7, A8, A9, A10, A11, Th5;
A16: b1 + b2 is Element of Bags n by POLYNOM1:def 14;
A17: for u being set st u in Support (p *' q) holds
u in {(b1 + b2)}

proof

let u be set ; :: thesis: ( u in Support (p *' q) implies u in {(b1 + b2)} )
assume A18: u in Support (p *' q) ; :: thesis: u in {(b1 + b2)}
assume A19: not u in {(b1 + b2)} ; :: thesis: contradiction
reconsider u = u as bag of by A18, POLYNOM1:def 14;
consider t being FinSequence of the carrier of L such that
A20: ( (p *' q) . u = Sum t & len t = len (decomp u) & ( for k being Element of NAT st k in dom t holds
ex b1', b2' being bag of st
( (decomp u) /. k = <*b1',b2'*> & t /. k = (p . b1') * (q . b2') ) ) ) by POLYNOM1:def 26;
1 <= len t by A20, NAT_1:14;
then A21: 1 in dom t by FINSEQ_3:27;
A22: dom t = Seg (len t) by FINSEQ_1:def 3
.= dom (decomp u) by A20, FINSEQ_1:def 3 ;
A23: for i being Element of NAT st i in dom t holds
t /. i = 0. L

proof

let i be Element of NAT ; :: thesis: ( i in dom t implies t /. i = 0. L )
assume A24: i in dom t ; :: thesis: t /. i = 0. L
then consider b1', b2' being bag of such that
A25: ( (decomp u) /. i = <*b1',b2'*> & t /. i = (p . b1') * (q . b2') ) by A20;
A26: b1' = (divisors u) /. i by A22, A24, A25, POLYNOM1:74;
consider S being non empty finite Subset of (Bags n) such that
A27: ( divisors u = SgmX (BagOrder n),S & ( for b being bag of holds
( b in S iff b divides u ) ) ) by POLYNOM1:def 18;
BagOrder n linearly_orders S by Lm3;
then A28: S = rng (divisors u) by A27, TRIANG_1:def 2;
A29: i in dom (divisors u) by A22, A24, POLYNOM1:def 19;
then b1' = (divisors u) . i by A26, PARTFUN1:def 8;
then b1' in rng (divisors u) by A29, FUNCT_1:def 5;
then A30: b1' divides u by A27, A28;

per cases ( ( b1' = b1 & b2' = b2 ) or b1' <> b1 or b2' <> b2 ) ;

suppose A31: ( b1' = b1 & b2' = b2 ) ; :: thesis: t /. i = 0. L

b2 = <*b1,b2*> . 2 by FINSEQ_1:61
.= <*b1,(u -' b1)*> . 2 by A22, A24, A25, A26, A31, POLYNOM1:def 19
.= u -' b1 by FINSEQ_1:61 ;
then b1 + b2 = u by A30, A31, POLYNOM1:51;
hence t /. i = 0. L by A19, TARSKI:def 1; :: thesis: verum

end;

suppose b1' <> b1 ; :: thesis: t /. i = 0. L

then p . b1' = 0. L by A2;
hence t /. i = 0. L by A25, VECTSP_1:39; :: thesis: verum

end;

suppose b2' <> b2 ; :: thesis: t /. i = 0. L

then q . b2' = 0. L by A4;
hence t /. i = 0. L by A25, VECTSP_1:39; :: thesis: verum

end;

end;

end;

then for i being Element of NAT st i in dom t & i <> 1 holds
t /. i = 0. L ;
then Sum t = t /. 1 by A21, Th5
.= 0. L by A21, A23 ;
hence contradiction by A18, A20, POLYNOM1:def 9; :: thesis: verum

end;

A32: ((p . b1) * (q . b2)) * ((eval b1,x) * (eval b2,x)) = (((p . b1) * (q . b2)) * (eval b1,x)) * (eval b2,x) by GROUP_1:def 4
.= (((p . b1) * (eval b1,x)) * (q . b2)) * (eval b2,x) by GROUP_1:def 4
.= ((p . b1) * (eval b1,x)) * ((q . b2) * (eval b2,x)) by GROUP_1:def 4
.= (eval p,x) * ((q . b2) * (eval b2,x)) by A1, Th21
.= (eval p,x) * (eval q,x) by A1, Th21 ;

per cases ( (p . b1) * (q . b2) = 0. L or (p . b1) * (q . b2) <> 0. L ) ;

suppose A33: (p . b1) * (q . b2) = 0. L ; :: thesis: eval (p *' q),x = (eval p,x) * (eval q,x)

then A34: not b1 + b2 in Support (p *' q) by A15, POLYNOM1:def 9;
Support (p *' q) = {}

proof

consider u being Element of Support (p *' q);
assume A35: Support (p *' q) <> {} ; :: thesis: contradiction
then A36: u in Support (p *' q) ;
u in {(b1 + b2)} by A17, A35;
hence contradiction by A34, A36, TARSKI:def 1; :: thesis: verum

end;

then p *' q = 0_ n,L by Th19;
hence eval (p *' q),x = 0. L by Th22
.= (eval p,x) * (eval q,x) by A32, A33, VECTSP_1:39 ;
:: thesis: verum

end;

suppose (p . b1) * (q . b2) <> 0. L ; :: thesis: eval (p *' q),x = (eval p,x) * (eval q,x)

then b1 + b2 in Support (p *' q) by A15, A16, POLYNOM1:def 9;
then for u being set st u in {(b1 + b2)} holds
u in Support (p *' q) by TARSKI:def 1;
then Support (p *' q) = {(b1 + b2)} by A17, TARSKI:2;
hence eval (p *' q),x = ((p *' q) . (b1 + b2)) * (eval (b1 + b2),x) by Th21
.= (eval p,x) * (eval q,x) by A15, A32, Th18 ;
:: thesis: verum

end;

end;