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, q be Polynomial of n,L; :: thesis:
let x be Function of n,L; :: thesis:
defpred S₁[ Element of 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 Element of NAT st S₁[k] holds
S₁[k + 1]

proof

proof

let u be set ; :: 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

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

end;

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

end;

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

proof

let u be set ; :: 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 9;

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)) by FUNCOP_1:19;
then p9 . u = p . u by A9, FUNCT_4:12;
then u in Support p9 by A15, POLYNOM1:def 9;
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)) by FUNCOP_1:19;
then p9 . bg = (bg .--> (0. L)) . bg by A9, FUNCT_4:14;
then A16: p9 . bg = 0. L by FUNCOP_1:87;
then A17: not bg in Support p9 by POLYNOM1:def 9;
for u being set st u in (Support p9) \/ {bg} holds
u in Support p

proof

let u be set ; :: 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 9;
then not u in {bg} by TARSKI:def 1;
then not u in dom (bg .--> (0. L)) by FUNCOP_1:19;
then A20: p9 . u = p . u by A9, FUNCT_4:12;
p9 . u <> 0. L by A19, POLYNOM1:def 9;
hence u in Support p by A20, POLYNOM1:def 9; :: thesis:

end;

suppose u in {bg} ; :: thesis:

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

end;

proof

let u be set ; :: 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 9;

now

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

end;

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

end;

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

proof

let u be set ; :: thesis:
bg in {bg} by TARSKI:def 1;
then bg in dom (bg .--> (p . bg)) by FUNCOP_1:19;
then m . bg = (bg .--> (p . bg)) . bg by A22, FUNCT_4:14;
then A26: m . bg = p . bg by FUNCOP_1:87;
assume u in {bg} ; :: thesis:
then u = bg by TARSKI:def 1;
hence u in Support m by A8, A26, POLYNOM1:def 9; :: thesis:

end;

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

proof

let u be set ; :: 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)) by FUNCOP_1:19;
then m . bg = (bg .--> (p . bg)) . bg by A22, FUNCT_4:14;
then A30: m . bg = p . bg by FUNCOP_1:87;
u in {bg} by A29, TARSKI:def 1;
then u in dom (bg .--> (0. L)) by FUNCOP_1:19;
then A31: p9 . u = (bg .--> (0. L)) . bg by A9, A29, FUNCT_4:14;
(p9 + m) . u = (p9 . u) + (m . u) by POLYNOM1:def 21
.= (0. L) + (p . bg) by A29, A31, A30, FUNCOP_1:87
.= p . bg by RLVECT_1:def 7 ;
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)) by FUNCOP_1:19;
not u in dom (bg .--> (p . bg)) by A32, FUNCOP_1:19;
then m . u = (0_ n,L) . u by A22, FUNCT_4:12;
then A34: m . u = 0. L by POLYNOM1:81;
(p9 + m) . u = (p9 . u) + (m . u) by POLYNOM1:def 21
.= (p . u) + (0. L) by A9, A33, A34, FUNCT_4:12
.= p . u by RLVECT_1:def 7 ;
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:9
.= (eval p9,x) + (eval m,x) by A27, Lm11 ;
hence (eval p,x) + (eval q,x) = ((eval p9,x) + (eval q,x)) + (eval m,x) by RLVECT_1:def 6
.= (eval (p9 + q),x) + (eval m,x) by A3, A21
.= eval (m + (p9 + q)),x by A27, Lm11
.= eval ((p9 + m) + q),x by POLYNOM1:80
.= eval (p + q),x by A35, A12, A28, FUNCT_1:9 ;
:: 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 Th19;
hence eval (p + q),x = eval q,x by POLYNOM1:82
.= (0. L) + (eval q,x) by RLVECT_1:10
.= (eval p,x) + (eval q,x) by A37, Th22 ;
:: thesis:

end;

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