let n be Ordinal; :: thesis:
let L be 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 4;
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:15
.= (0. L) + (q . b9) by A5, A4, POLYNOM1:def 4
.= q . b9 by RLVECT_1:def 4 ; :: 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:20;
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 Def2;
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 Def2;
A14: BagOrder n linearly_orders Support q by Th10;

now :: thesis:

per cases ;

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

now :: thesis:

per cases ;

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

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

proof

let u be object ; :: 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 4;
u is Element of Bags n by PRE_POLY:def 12;
then u in Support (p + q) by A19, POLYNOM1:def 4;
hence u in (Support (p + q)) \/ {b} by XBOOLE_0:def 3; :: thesis:

end;

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

proof

let u be object ; :: 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 4
.= (eval ((p + q),x)) + (((q . b) * (eval (b,x))) + (- ((q . b) * (eval (b,x))))) by RLVECT_1:5
.= ((eval ((p + q),x)) + ((q . b) * (eval (b,x)))) + (- ((q . b) * (eval (b,x)))) by RLVECT_1:def 3
.= (eval (q,x)) + (- ((q . b) * (eval (b,x)))) by A3, A20, A23, Lm6
.= (eval (q,x)) + ((p . b) * (eval (b,x))) by A16, VECTSP_1:9
.= (eval (q,x)) + (eval (p,x)) by A1, Th11 ; :: 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 4
.= (p . b) + ((q . b) + (- (q . b))) by RLVECT_1:5
.= ((- (q . b)) + (q . b)) + (- (q . b)) by A25, RLVECT_1:def 3
.= (0. L) + (- (q . b)) by RLVECT_1:5
.= - (q . b) by RLVECT_1:def 4 ;
hence contradiction by A24; :: thesis:

end;

then (p . b) + (q . b) <> 0. L by RLVECT_1:5;
then A26: (p + q) . b <> 0. L by POLYNOM1:15;
A27: for u being object st u in Support q holds
u in Support (p + q)

proof

let u be object ; :: 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 4; :: 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 4;
u is Element of Bags n by PRE_POLY:def 12;
hence u in Support (p + q) by A29, POLYNOM1:def 4; :: thesis:

end;

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

proof

let u be object ; :: 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 6;
A59: SgmX ((BagOrder n),(Support (p + q))) is one-to-one by Th10, 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 4; :: thesis:

end;

end;

A64: (SgmX ((BagOrder n),(Support q))) /. k = b by A35, A36, PARTFUN1:def 6;
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:1;
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:15
.= ((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 7
.= ((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, Th4
.= (eval (p,x)) + (eval (q,x)) by A1, A9, Th11 ;
:: 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:15
.= (p . b) + (0. L) by A6, A67, POLYNOM1:def 4
.= p . b by RLVECT_1:def 4 ;
A69: for u being object st u in (Support p) \/ (Support q) holds
u in Support (p + q)

proof

let u be object ; :: 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 4; :: 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 4;
(p + q) . u = q . u by A3, A67, A71;
hence u in Support (p + q) by A71, A72, POLYNOM1:def 4; :: thesis:

end;

for u being object 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, Lm6
.= (eval (q,x)) + (eval (p,x)) by A1, A68, Th11 ;
:: thesis:

end;

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