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 n 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 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 n 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 n 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 n; :: 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 that
A1: Support p = {b1} and
A2: Support q = {b2} ; :: thesis: for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
consider s being FinSequence of the carrier of L such that
A3: (p *' q) . (b1 + b2) = Sum s and
A4: len s = len (decomp (b1 + b2)) and
A5: for k being Element of NAT st k in dom s holds
ex u1, u2 being bag of n st
( (decomp (b1 + b2)) /. k = <*u1,u2*> & s /. k = (p . u1) * (q . u2) ) by POLYNOM1:def 10;
A6: b1 + b2 is Element of Bags n by PRE_POLY:def 12;
let x be Function of n,L; :: thesis: eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
A7: ((p . b1) * (q . b2)) * ((eval (b1,x)) * (eval (b2,x))) = (((p . b1) * (q . b2)) * (eval (b1,x))) * (eval (b2,x)) by GROUP_1:def 3
.= (((p . b1) * (eval (b1,x))) * (q . b2)) * (eval (b2,x)) by GROUP_1:def 3
.= ((p . b1) * (eval (b1,x))) * ((q . b2) * (eval (b2,x))) by GROUP_1:def 3
.= (eval (p,x)) * ((q . b2) * (eval (b2,x))) by A1, Th11
.= (eval (p,x)) * (eval (q,x)) by A2, Th11 ;
A8: for b being bag of n st b <> b2 holds
q . b = 0. L

proof

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

end;

A10: for b being bag of n st b <> b1 holds
p . b = 0. L

proof

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

end;

A12: for u being object st u in Support (p *' q) holds
u in {(b1 + b2)}

proof

let u be object ; :: thesis: ( u in Support (p *' q) implies u in {(b1 + b2)} )
assume A13: u in Support (p *' q) ; :: thesis: u in {(b1 + b2)}
assume A14: not u in {(b1 + b2)} ; :: thesis: contradiction
reconsider u = u as bag of n by A13;
consider t being FinSequence of the carrier of L such that
A15: (p *' q) . u = Sum t and
A16: len t = len (decomp u) and
A17: for k being Element of NAT st k in dom t holds
ex b19, b29 being bag of n st
( (decomp u) /. k = <*b19,b29*> & t /. k = (p . b19) * (q . b29) ) by POLYNOM1:def 10;
1 <= len t by A16, NAT_1:14;
then A18: 1 in dom t by FINSEQ_3:25;
A19: dom t = Seg (len t) by FINSEQ_1:def 3
.= dom (decomp u) by A16, FINSEQ_1:def 3 ;
A20: 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 )
consider S being non empty finite Subset of (Bags n) such that
A21: divisors u = SgmX ((BagOrder n),S) and
A22: for b being bag of n holds
( b in S iff b divides u ) by PRE_POLY:def 16;
BagOrder n linearly_orders S by Lm3;
then A23: S = rng (divisors u) by A21, PRE_POLY:def 2;
assume A24: i in dom t ; :: thesis: t /. i = 0. L
then consider b19, b29 being bag of n such that
A25: (decomp u) /. i = <*b19,b29*> and
A26: t /. i = (p . b19) * (q . b29) by A17;
A27: b19 = (divisors u) /. i by A19, A24, A25, PRE_POLY:70;
A28: i in dom (divisors u) by A19, A24, PRE_POLY:def 17;
then b19 = (divisors u) . i by A27, PARTFUN1:def 6;
then b19 in rng (divisors u) by A28, FUNCT_1:def 3;
then A29: b19 divides u by A22, A23;

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

suppose A30: ( b19 = b1 & b29 = b2 ) ; :: thesis: t /. i = 0. L

b2 = <*b1,b2*> . 2
.= <*b1,(u -' b1)*> . 2 by A19, A24, A25, A27, A30, PRE_POLY:def 17
.= u -' b1 ;
then b1 + b2 = u by A29, A30, PRE_POLY:47;
hence t /. i = 0. L by A14, TARSKI:def 1; :: thesis: verum

end;

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

then p . b19 = 0. L by A10;
hence t /. i = 0. L by A26; :: thesis: verum

end;

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

then q . b29 = 0. L by A8;
hence t /. i = 0. L by A26; :: 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 A18, Th2
.= 0. L by A18, A20 ;
hence contradiction by A13, A15, POLYNOM1:def 4; :: thesis: verum

end;

consider k being Element of NAT such that
A31: k in dom (decomp (b1 + b2)) and
A32: (decomp (b1 + b2)) /. k = <*b1,b2*> by PRE_POLY:69;
A33: dom s = Seg (len s) by FINSEQ_1:def 3
.= dom (decomp (b1 + b2)) by A4, FINSEQ_1:def 3 ;
then consider b19, b29 being bag of n such that
A34: (decomp (b1 + b2)) /. k = <*b19,b29*> and
A35: s /. k = (p . b19) * (q . b29) by A5, A31;
A36: b2 = <*b1,b2*> . 2
.= b29 by A32, A34, FINSEQ_1:44 ;
A37: for k9 being Element of NAT st k9 in dom s & k9 <> k holds
s /. k9 = 0. L

proof

let k9 be Element of NAT ; :: thesis: ( k9 in dom s & k9 <> k implies s /. k9 = 0. L )
assume that
A38: k9 in dom s and
A39: k9 <> k ; :: thesis: s /. k9 = 0. L
consider b19, b29 being bag of n such that
A40: (decomp (b1 + b2)) /. k9 = <*b19,b29*> and
A41: s /. k9 = (p . b19) * (q . b29) by A5, A38;

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

suppose A42: ( b19 = b1 & b29 = b2 ) ; :: thesis: s /. k9 = 0. L

(decomp (b1 + b2)) . k9 = (decomp (b1 + b2)) /. k9 by A33, A38, PARTFUN1:def 6
.= (decomp (b1 + b2)) . k by A31, A32, A40, A42, PARTFUN1:def 6 ;
hence s /. k9 = 0. L by A33, A31, A38, A39, FUNCT_1:def 4; :: thesis: verum

end;

suppose b19 <> b1 ; :: thesis: s /. k9 = 0. L

then p . b19 = 0. L by A10;
hence s /. k9 = 0. L by A41; :: thesis: verum

end;

suppose b29 <> b2 ; :: thesis: s /. k9 = 0. L

then q . b29 = 0. L by A8;
hence s /. k9 = 0. L by A41; :: thesis: verum

end;

end;

end;

b1 = <*b19,b29*> . 1 by A32, A34
.= b19 ;
then A43: (p *' q) . (b1 + b2) = (p . b1) * (q . b2) by A3, A33, A31, A35, A36, A37, Th2;

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

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

then A45: not b1 + b2 in Support (p *' q) by A43, POLYNOM1:def 4;
Support (p *' q) = {}

proof

set u = the Element of Support (p *' q);
assume A46: Support (p *' q) <> {} ; :: thesis: contradiction
then A47: the Element of Support (p *' q) in Support (p *' q) ;
the Element of Support (p *' q) in {(b1 + b2)} by A12, A46;
hence contradiction by A45, A47, TARSKI:def 1; :: thesis: verum

end;

then p *' q = 0_ (n,L) by Th9;
hence eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) by A7, A44, Th12; :: 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 A43, A6, POLYNOM1:def 4;
then for u being object st u in {(b1 + b2)} holds
u in Support (p *' q) by TARSKI:def 1;
then Support (p *' q) = {(b1 + b2)} by A12, TARSKI:2;
hence eval ((p *' q),x) = ((p *' q) . (b1 + b2)) * (eval ((b1 + b2),x)) by Th11
.= (eval (p,x)) * (eval (q,x)) by A43, A7, Th8 ;
:: thesis: verum

end;

end;