let n be Ordinal; :: thesis:
let L be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis:
let p, q be Polynomial of n,L; :: thesis:
let x be Function of n,L; :: thesis:
defpred S₁[ Nat] means for p being Polynomial of n,L st card (Support p) = $1 holds
eval ((p + q),x) = (eval (p,x)) + (eval (q,x));
A1: ex k being Element of NAT st card (Support p) = k ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

proof

let u be object ; :: thesis:
assume A10: u in Support p9 ; :: thesis:
then reconsider u = u as Element of Bags n ;
reconsider u = u as bag of n ;

now :: thesis:

assume A11: u = bg ; :: thesis:
then u in {bg} by TARSKI:def 1;
then u in dom (bg .--> (0. L)) ;
then p9 . u = (bg .--> (0. L)) . bg by A9, A11, FUNCT_4:13;
then p9 . u = 0. L by FUNCOP_1:72;
hence contradiction by A10, POLYNOM1:def 4; :: thesis:

end;

then not u in {bg} by TARSKI:def 1;
then not u in dom (bg .--> (0. L)) ;
then p . u = p9 . u by A9, FUNCT_4:11;
then p . u <> 0. L by A10, POLYNOM1:def 4;
hence u in Support p by POLYNOM1:def 4; :: thesis:

end;

then Support p9 c= Support p by TARSKI:def 3;
then reconsider p9 = p9 as Polynomial of n,L by POLYNOM1:def 5;
A12: dom p = Bags n by FUNCT_2:def 1;
A13: for u being object st u in Support p holds
u in (Support p9) \/ {bg}

proof

let u be object ; :: thesis:
assume A14: u in Support p ; :: thesis:
then reconsider u = u as Element of Bags n ;
A15: p . u <> 0. L by A14, POLYNOM1:def 4;

per cases ;

suppose u = bg ; :: thesis:

then u in {bg} by TARSKI:def 1;
hence u in (Support p9) \/ {bg} by XBOOLE_0:def 3; :: thesis:

end;

suppose u <> bg ; :: thesis:

then not u in {bg} by TARSKI:def 1;
then not u in dom (bg .--> (0. L)) ;
then p9 . u = p . u by A9, FUNCT_4:11;
then u in Support p9 by A15, POLYNOM1:def 4;
hence u in (Support p9) \/ {bg} by XBOOLE_0:def 3; :: thesis:

end;

bg in {bg} by TARSKI:def 1;
then bg in dom (bg .--> (0. L)) ;
then p9 . bg = (bg .--> (0. L)) . bg by A9, FUNCT_4:13;
then A16: p9 . bg = 0. L by FUNCOP_1:72;
then A17: not bg in Support p9 by POLYNOM1:def 4;
for u being object st u in (Support p9) \/ {bg} holds
u in Support p

proof

let u be object ; :: thesis:
assume A18: u in (Support p9) \/ {bg} ; :: thesis:

per cases by A18, XBOOLE_0:def 3;

suppose A19: u in Support p9 ; :: thesis:

then reconsider u = u as Element of Bags n ;
u <> bg by A16, A19, POLYNOM1:def 4;
then not u in {bg} by TARSKI:def 1;
then not u in dom (bg .--> (0. L)) ;
then A20: p9 . u = p . u by A9, FUNCT_4:11;
p9 . u <> 0. L by A19, POLYNOM1:def 4;
hence u in Support p by A20, POLYNOM1:def 4; :: thesis:

end;

suppose u in {bg} ; :: thesis:

hence u in Support p by A7, TARSKI:def 1; :: thesis:

end;

then Support p = (Support p9) \/ {bg} by A13, TARSKI:2;
then A21: k + 1 = (card (Support p9)) + 1 by A4, A17, CARD_2:41;
dom (0_ (n,L)) = Bags n by FUNCT_2:def 1;
then A22: (0_ (n,L)) +* (((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))),(p . ((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))))) = (0_ (n,L)) +* (bg .--> (p . bg)) by FUNCT_7:def 3;
reconsider m = (0_ (n,L)) +* (((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))),(p . ((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))))) as Function of (Bags n), the carrier of L ;
reconsider m = m as Function of (Bags n),L ;
A23: for u being object st u in Support m holds
u in {bg}

proof

let u be object ; :: thesis:
assume A24: u in Support m ; :: thesis:
then reconsider u = u as Element of Bags n ;
A25: m . u <> 0. L by A24, POLYNOM1:def 4;

now :: thesis:

assume u <> bg ; :: thesis:
then not u in {bg} by TARSKI:def 1;
then not u in dom (bg .--> (p . bg)) ;
then m . u = (0_ (n,L)) . u by A22, FUNCT_4:11;
hence contradiction by A25, POLYNOM1:22; :: thesis:

end;

hence u in {bg} by TARSKI:def 1; :: thesis:

end;

for u being object st u in {bg} holds
u in Support m

proof

let u be object ; :: thesis:
bg in {bg} by TARSKI:def 1;
then bg in dom (bg .--> (p . bg)) ;
then m . bg = (bg .--> (p . bg)) . bg by A22, FUNCT_4:13;
then A26: m . bg = p . bg by FUNCOP_1:72;
assume u in {bg} ; :: thesis:
then u = bg by TARSKI:def 1;
hence u in Support m by A8, A26, POLYNOM1:def 4; :: thesis:

end;

then A27: Support m = {bg} by A23, TARSKI:2;
then reconsider m = m as Polynomial of n,L by POLYNOM1:def 5;
reconsider m = m as Polynomial of n,L ;
A28: for u being object st u in Bags n holds
(p9 + m) . u = p . u

proof

let u be object ; :: thesis:
assume u in Bags n ; :: thesis:
then reconsider u = u as bag of n ;

per cases ;

suppose A29: u = bg ; :: thesis:

bg in {bg} by TARSKI:def 1;
then bg in dom (bg .--> (p . bg)) ;
then m . bg = (bg .--> (p . bg)) . bg by A22, FUNCT_4:13;
then A30: m . bg = p . bg by FUNCOP_1:72;
u in {bg} by A29, TARSKI:def 1;
then u in dom (bg .--> (0. L)) ;
then A31: p9 . u = (bg .--> (0. L)) . bg by A9, A29, FUNCT_4:13;
(p9 + m) . u = (p9 . u) + (m . u) by POLYNOM1:15
.= (0. L) + (p . bg) by A29, A31, A30, FUNCOP_1:72
.= p . bg by RLVECT_1:def 4 ;
hence (p9 + m) . u = p . u by A29; :: thesis:

end;

suppose u <> bg ; :: thesis:

then A32: not u in {bg} by TARSKI:def 1;
then A33: not u in dom (bg .--> (0. L)) ;
not u in dom (bg .--> (p . bg)) by A32;
then m . u = (0_ (n,L)) . u by A22, FUNCT_4:11;
then A34: m . u = 0. L by POLYNOM1:22;
(p9 + m) . u = (p9 . u) + (m . u) by POLYNOM1:15
.= (p . u) + (0. L) by A9, A33, A34, FUNCT_4:11
.= p . u by RLVECT_1:def 4 ;
hence (p9 + m) . u = p . u ; :: thesis:

end;

A35: dom (p9 + m) = Bags n by FUNCT_2:def 1;
then eval (p,x) = eval ((m + p9),x) by A12, A28, FUNCT_1:2
.= (eval (p9,x)) + (eval (m,x)) by A27, Lm7 ;
hence (eval (p,x)) + (eval (q,x)) = ((eval (p9,x)) + (eval (q,x))) + (eval (m,x)) by RLVECT_1:def 3
.= (eval ((p9 + q),x)) + (eval (m,x)) by A3, A21
.= eval ((m + (p9 + q)),x) by A27, Lm7
.= eval (((p9 + m) + q),x) by POLYNOM1:21
.= eval ((p + q),x) by A35, A12, A28, FUNCT_1:2 ;
:: thesis:

end;

A36: S₁[ 0 ]

proof

let p be Polynomial of n,L; :: thesis:
assume card (Support p) = 0 ; :: thesis:
then Support p = {} ;
then A37: p = 0_ (n,L) by Th9;
hence eval ((p + q),x) = eval (q,x) by POLYNOM1:23
.= (0. L) + (eval (q,x)) by RLVECT_1:4
.= (eval (p,x)) + (eval (q,x)) by A37, Th12 ;
:: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A36, A2);
hence eval ((p + q),x) = (eval (p,x)) + (eval (q,x)) by A1; :: thesis: