let n be Ordinal; :: thesis:
let L be non empty non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis:
let p be Polynomial of n,L; :: thesis:
assume ex b being bag of n st Support p = {b} ; :: thesis:
then consider b being bag of n such that
A1: Support p = {b} ;
b in Support p by A1, TARSKI:def 1;
then A2: p . b <> 0. L by POLYNOM1:def 9;
let q be Polynomial of n,L; :: thesis:
let x be Function of n,L; :: thesis:
A3: for b9 being bag of n st b9 <> b holds
(p + q) . b9 = q . b9

proof

let b9 be bag of n; :: thesis:
A4: b9 is Element of Bags n by PRE_POLY:def 12;
assume b9 <> b ; :: thesis:
then A5: not b9 in Support p by A1, TARSKI:def 1;
thus (p + q) . b9 = (p . b9) + (q . b9) by POLYNOM1:def 21
.= (0. L) + (q . b9) by A5, A4, POLYNOM1:def 9
.= q . b9 by RLVECT_1:def 7 ; :: thesis:

end;

set sq = SgmX (BagOrder n),(Support q);
set spq = SgmX (BagOrder n),(Support (p + q));
A6: b is Element of Bags n by PRE_POLY:def 12;
A7: Support (p + q) c= (Support p) \/ (Support q) by POLYNOM1:79;
consider yq being FinSequence of the carrier of L such that
A8: len yq = len (SgmX (BagOrder n),(Support q)) and
A9: eval q,x = Sum yq and
A10: for i being Element of NAT st 1 <= i & i <= len yq holds
yq /. i = ((q * (SgmX (BagOrder n),(Support q))) /. i) * (eval (((SgmX (BagOrder n),(Support q)) /. i) @ ),x) by Def4;
consider ypq being FinSequence of the carrier of L such that
A11: len ypq = len (SgmX (BagOrder n),(Support (p + q))) and
A12: eval (p + q),x = Sum ypq and
A13: for i being Element of NAT st 1 <= i & i <= len ypq holds
ypq /. i = (((p + q) * (SgmX (BagOrder n),(Support (p + q)))) /. i) * (eval (((SgmX (BagOrder n),(Support (p + q))) /. i) @ ),x) by Def4;
A14: BagOrder n linearly_orders Support q by Th20;

now

per cases ;

case A15: b in Support q ; :: thesis:

now

per cases ;

case A16: p . b = - (q . b) ; :: thesis:

A17: for u being set st u in Support q holds
u in (Support (p + q)) \/ {b}

proof

let u be set ; :: thesis:
assume A18: u in Support q ; :: thesis:
then reconsider u = u as bag of n ;

per cases ;

suppose u = b ; :: thesis:

then u in {b} by TARSKI:def 1;
hence u in (Support (p + q)) \/ {b} by XBOOLE_0:def 3; :: thesis:

end;

suppose u <> b ; :: thesis:

then (p + q) . u = q . u by A3;
then A19: (p + q) . u <> 0. L by A18, POLYNOM1:def 9;
u is Element of Bags n by PRE_POLY:def 12;
then u in Support (p + q) by A19, POLYNOM1:def 9;
hence u in (Support (p + q)) \/ {b} by XBOOLE_0:def 3; :: thesis:

end;

(p + q) . b = (p . b) + (q . b) by POLYNOM1:def 21
.= 0. L by A16, RLVECT_1:16 ;
then A20: not b in Support (p + q) by POLYNOM1:def 9;
for u being set st u in (Support (p + q)) \/ {b} holds
u in Support q

proof

let u be set ; :: thesis:
assume A21: u in (Support (p + q)) \/ {b} ; :: thesis:

per cases by A21, XBOOLE_0:def 3;

suppose A22: u in Support (p + q) ; :: thesis:

then not u in {b} by A20, TARSKI:def 1;
hence u in Support q by A1, A7, A22, XBOOLE_0:def 3; :: thesis:

end;

suppose u in {b} ; :: thesis:

hence u in Support q by A15, TARSKI:def 1; :: thesis:

end;

then A23: (Support (p + q)) \/ {b} = Support q by A17, TARSKI:2;
thus eval (p + q),x = (eval (p + q),x) + (0. L) by RLVECT_1:def 7
.= (eval (p + q),x) + (((q . b) * (eval b,x)) + (- ((q . b) * (eval b,x)))) by RLVECT_1:16
.= ((eval (p + q),x) + ((q . b) * (eval b,x))) + (- ((q . b) * (eval b,x))) by RLVECT_1:def 6
.= (eval q,x) + (- ((q . b) * (eval b,x))) by A3, A20, A23, Lm10
.= (eval q,x) + ((p . b) * (eval b,x)) by A16, VECTSP_1:41
.= (eval q,x) + (eval p,x) by A1, Th21 ; :: thesis:

end;

case A24: p . b <> - (q . b) ; :: thesis:

(p . b) + (q . b) <> (- (q . b)) + (q . b)

proof

assume A25: (p . b) + (q . b) = (- (q . b)) + (q . b) ; :: thesis:
p . b = (p . b) + (0. L) by RLVECT_1:def 7
.= (p . b) + ((q . b) + (- (q . b))) by RLVECT_1:16
.= ((- (q . b)) + (q . b)) + (- (q . b)) by A25, RLVECT_1:def 6
.= (0. L) + (- (q . b)) by RLVECT_1:16
.= - (q . b) by RLVECT_1:def 7 ;
hence contradiction by A24; :: thesis:

end;

then (p . b) + (q . b) <> 0. L by RLVECT_1:16;
then A26: (p + q) . b <> 0. L by POLYNOM1:def 21;
A27: for u being set st u in Support q holds
u in Support (p + q)

proof

let u be set ; :: thesis:
assume A28: u in Support q ; :: thesis:
then reconsider u = u as bag of n ;

per cases ;

suppose u = b ; :: thesis:

hence u in Support (p + q) by A6, A26, POLYNOM1:def 9; :: thesis:

end;

suppose u <> b ; :: thesis:

then (p + q) . u = q . u by A3;
then A29: (p + q) . u <> 0. L by A28, POLYNOM1:def 9;
u is Element of Bags n by PRE_POLY:def 12;
hence u in Support (p + q) by A29, POLYNOM1:def 9; :: thesis:

end;

A30: for u being set st u in Support (p + q) holds
u in Support q

proof

let u be set ; :: thesis:
assume A31: u in Support (p + q) ; :: thesis:
then reconsider u = u as bag of n ;

per cases by A7, A31, XBOOLE_0:def 3;

suppose u in Support p ; :: thesis:

hence u in Support q by A1, A15, TARSKI:def 1; :: thesis:

end;

suppose u in Support q ; :: thesis:

hence u in Support q ; :: thesis:

end;

proof

proof

assume (SgmX (BagOrder n),(Support (p + q))) /. i9 = b ; :: thesis:
then A58: (SgmX (BagOrder n),(Support (p + q))) . i9 = b by A54, PARTFUN1:def 8;
A59: SgmX (BagOrder n),(Support (p + q)) is one-to-one by Th20, PRE_POLY:10;
(SgmX (BagOrder n),(Support (p + q))) . k = b by A30, A27, A36, TARSKI:2;
hence contradiction by A35, A37, A34, A47, A52, A54, A58, A59, FUNCT_1:def 8; :: thesis:

end;

end;

A64: (SgmX (BagOrder n),(Support q)) /. k = b by A35, A36, PARTFUN1:def 8;
A65: sqk = len yq by A8, A37, FINSEQ_1:def 3;
then k <= i by A42, A46, A48, FINSEQ_1:def 3;
then A66: k in dom yq by A38, A46, FINSEQ_1:3;
len ypq = sqk by A11, A34, A47, FINSEQ_1:def 3;
then ypq /. k = (((p + q) * (SgmX (BagOrder n),(Support (p + q)))) /. k) * (eval (((SgmX (BagOrder n),(Support (p + q))) /. k) @ ),x) by A13, A38, A42
.= ((p . b) + (q . b)) * (eval b,x) by A32, A64, A41, POLYNOM1:def 21
.= ((p . b) * (eval b,x)) + (((q * (SgmX (BagOrder n),(Support q))) /. k) * (eval (((SgmX (BagOrder n),(Support q)) /. k) @ ),x)) by A64, A45, VECTSP_1:def 18
.= ((p . b) * (eval b,x)) + (yq /. k) by A10, A38, A42, A65 ;
hence eval (p + q),x = ((p . b) * (eval b,x)) + (Sum yq) by A12, A33, A66, A50, Th7
.= (eval p,x) + (eval q,x) by A1, A9, Th21 ;
:: thesis:

end;

hence eval (p + q),x = (eval p,x) + (eval q,x) ; :: thesis:

end;

case A67: not b in Support q ; :: thesis:

A68: (p + q) . b = (p . b) + (q . b) by POLYNOM1:def 21
.= (p . b) + (0. L) by A6, A67, POLYNOM1:def 9
.= p . b by RLVECT_1:def 7 ;
A69: for u being set st u in (Support p) \/ (Support q) holds
u in Support (p + q)

proof

let u be set ; :: thesis:
assume A70: u in (Support p) \/ (Support q) ; :: thesis:

per cases by A70, XBOOLE_0:def 3;

suppose u in Support p ; :: thesis:

then u = b by A1, TARSKI:def 1;
hence u in Support (p + q) by A6, A2, A68, POLYNOM1:def 9; :: thesis:

end;

suppose A71: u in Support q ; :: thesis:

then reconsider u = u as bag of n ;
A72: q . u <> 0. L by A71, POLYNOM1:def 9;
(p + q) . u = q . u by A3, A67, A71;
hence u in Support (p + q) by A71, A72, POLYNOM1:def 9; :: thesis:

end;

for u being set st u in Support (p + q) holds
u in (Support p) \/ (Support q) by A7;
then Support (p + q) = {b} \/ (Support q) by A1, A69, TARSKI:2;
hence eval (p + q),x = (eval q,x) + (((p + q) . b) * (eval b,x)) by A3, A67, Lm10
.= (eval q,x) + (eval p,x) by A1, A68, Th21 ;
:: thesis:

end;

hence eval (p + q),x = (eval p,x) + (eval q,x) ; :: thesis: