let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of n,L
for x being Function of n,L
for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ) holds
eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))
let L be non empty non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p, q being Polynomial of n,L
for x being Function of n,L
for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ) holds
eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))
let p, q be Polynomial of n,L; :: thesis: for x being Function of n,L
for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ) holds
eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))
let x be Function of n,L; :: thesis: for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ) holds
eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))
let b be bag of n; :: thesis: ( not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ) implies eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x))) )
assume that
A1: not b in Support p and
A2: Support q = (Support p) \/ {b} and
A3: for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ; :: thesis: eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))
set sq = SgmX ((BagOrder n),(Support q));
set sp = SgmX ((BagOrder n),(Support p));
A4: BagOrder n linearly_orders Support q by Th20;
b in {b} by TARSKI:def 1;
then b in Support q by A2, XBOOLE_0:def 3;
then b in rng (SgmX ((BagOrder n),(Support q))) by A4, PRE_POLY:def 2;
then consider k being Nat such that
A5: k in dom (SgmX ((BagOrder n),(Support q))) and
A6: (SgmX ((BagOrder n),(Support q))) . k = b by FINSEQ_2:11;
A7: (SgmX ((BagOrder n),(Support q))) /. k = b by A5, A6, PARTFUN1:def 8;
reconsider b = b as Element of Bags n by PRE_POLY:def 12;
A8: dom (SgmX ((BagOrder n),(Support q))) = Seg (len (SgmX ((BagOrder n),(Support q)))) by FINSEQ_1:def 3;
then A9: k <= len (SgmX ((BagOrder n),(Support q))) by A5, FINSEQ_1:3;
1 <= k by A5, A8, FINSEQ_1:3;
then 1 - 1 <= k - 1 by XREAL_1:11;
then reconsider k9 = k - 1 as Element of NAT by INT_1:16;
A10: k9 + 1 = k + 0 ;
then A11: SgmX ((BagOrder n),(Support q)) = Ins ((SgmX ((BagOrder n),(Support p))),k9,b) by A1, A2, A5, A7, Th13, Th20;
consider yp being FinSequence of the carrier of L such that
A12: len yp = len (SgmX ((BagOrder n),(Support p))) and
A13: Sum yp = eval (p,x) and
A14: for i being Element of NAT st 1 <= i & i <= len yp holds
yp /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval ((((SgmX ((BagOrder n),(Support p))) /. i) @),x)) by Def4;
consider yq being FinSequence of the carrier of L such that
A15: len yq = len (SgmX ((BagOrder n),(Support q))) and
A16: Sum yq = eval (q,x) and
A17: 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;
reconsider b = b as Element of Bags n ;
set ytmp = Ins (yp,k9,((q . b) * (eval (b,x))));
A18: (len (SgmX ((BagOrder n),(Support p)))) + 1 = (card (Support p)) + 1 by Th20, PRE_POLY:11
.= card (Support q) by A1, A2, CARD_2:54
.= len (SgmX ((BagOrder n),(Support q))) by Th20, PRE_POLY:11 ;
then A19: len yq = len (Ins (yp,k9,((q . b) * (eval (b,x))))) by A15, A12, FINSEQ_5:72;
A20: BagOrder n linearly_orders Support p by Th20;
A21: for i being Nat st 1 <= i & i <= len yq holds
yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len yq implies yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i )
assume that
A22: 1 <= i and
A23: i <= len yq ; :: thesis: yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i
i in Seg (len yq) by A22, A23, FINSEQ_1:3;
then A24: i in dom yq by FINSEQ_1:def 3;
i in Seg (len (Ins (yp,k9,((q . b) * (eval (b,x)))))) by A19, A22, A23, FINSEQ_1:3;
then A25: i in dom (Ins (yp,k9,((q . b) * (eval (b,x))))) by FINSEQ_1:def 3;

per cases ( i = k or i <> k ) ;

suppose A26: i = k ; :: thesis: yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i

dom q = Bags n by FUNCT_2:def 1;
then (SgmX ((BagOrder n),(Support q))) . k in dom q by A6, PRE_POLY:def 12;
then A27: k in dom (q * (SgmX ((BagOrder n),(Support q)))) by A5, FUNCT_1:21;
then A28: (q * (SgmX ((BagOrder n),(Support q)))) /. k = (q * (SgmX ((BagOrder n),(Support q)))) . k by PARTFUN1:def 8
.= q . b by A6, A27, FUNCT_1:22 ;
A29: yq /. i = ((q * (SgmX ((BagOrder n),(Support q)))) /. k) * (eval ((((SgmX ((BagOrder n),(Support q))) /. k) @),x)) by A5, A17, A22, A23, A26
.= (q . b) * (eval (b,x)) by A5, A6, A28, PARTFUN1:def 8 ;
A30: k9 <= len yp by A9, A10, A12, A18, XREAL_1:8;
thus (Ins (yp,k9,((q . b) * (eval (b,x))))) . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) /. i by A25, PARTFUN1:def 8
.= (q . b) * (eval (b,x)) by A10, A26, A30, FINSEQ_5:76
.= yq . i by A24, A29, PARTFUN1:def 8 ; :: thesis: verum

end;

suppose A31: i <> k ; :: thesis: yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i

len (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) = (len (SgmX ((BagOrder n),(Support p)))) + 1 by FINSEQ_5:72;
then A32: dom (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) = Seg ((len (SgmX ((BagOrder n),(Support p)))) + 1) by FINSEQ_1:def 3;

now

per cases ( i < k or i > k ) by A31, XXREAL_0:1;

case A33: i < k ; :: thesis: yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i

k9 < k by A10, NAT_1:19;
then k9 < len yq by A9, A15, XXREAL_0:2;
then A34: k9 <= len yp by A15, A12, A18, NAT_1:13;
A35: yp | (Seg k9) is FinSequence by FINSEQ_1:19;
A36: i <= k9 by A10, A33, NAT_1:13;
then i in Seg k9 by A22, FINSEQ_1:3;
then i in dom (yp | (Seg k9)) by A34, A35, FINSEQ_1:21;
then A37: i in dom (yp | k9) by FINSEQ_1:def 15;
A38: k - 1 <= ((len (SgmX ((BagOrder n),(Support p)))) + 1) - 1 by A9, A18, XREAL_1:11;
then A39: i <= len (SgmX ((BagOrder n),(Support p))) by A36, XXREAL_0:2;
then i in Seg (len (SgmX ((BagOrder n),(Support p)))) by A22, FINSEQ_1:3;
then A40: i in dom (SgmX ((BagOrder n),(Support p))) by FINSEQ_1:def 3;

A41: now

assume (SgmX ((BagOrder n),(Support p))) /. i = b ; :: thesis: contradiction
then (SgmX ((BagOrder n),(Support p))) . i = b by A40, PARTFUN1:def 8;
then b in rng (SgmX ((BagOrder n),(Support p))) by A40, FUNCT_1:def 5;
hence contradiction by A1, A20, PRE_POLY:def 2; :: thesis: verum

end;

i < len yq by A9, A15, A33, XXREAL_0:2;
then A42: i <= len yp by A15, A12, A18, NAT_1:13;
A43: (SgmX ((BagOrder n),(Support p))) | (Seg k9) is FinSequence by FINSEQ_1:19;
A45: rng (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) c= Bags n by FINSEQ_1:def 4;
A46: dom q = Bags n by FUNCT_2:def 1;
A47: rng (SgmX ((BagOrder n),(Support p))) c= Bags n by FINSEQ_1:def 4;
i in Seg k9 by A22, A36, FINSEQ_1:3;
then i in dom ((SgmX ((BagOrder n),(Support p))) | (Seg k9)) by A38, A43, FINSEQ_1:21;
then A48: i in dom ((SgmX ((BagOrder n),(Support p))) | k9) by FINSEQ_1:def 15;
(SgmX ((BagOrder n),(Support p))) . i in rng (SgmX ((BagOrder n),(Support p))) by A40, FUNCT_1:def 5;
then (SgmX ((BagOrder n),(Support p))) . i in Bags n by A47;
then (SgmX ((BagOrder n),(Support p))) . i in dom p by FUNCT_2:def 1;
then A49: i in dom (p * (SgmX ((BagOrder n),(Support p)))) by A40, FUNCT_1:21;
len (SgmX ((BagOrder n),(Support p))) <= (len (SgmX ((BagOrder n),(Support p)))) + 1 by XREAL_1:31;
then i <= (len (SgmX ((BagOrder n),(Support p)))) + 1 by A39, XXREAL_0:2;
then A50: i in dom (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) by A22, A32, FINSEQ_1:3;
then (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) . i in rng (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) by FUNCT_1:def 5;
then A51: i in dom (q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))) by A50, A45, A46, FUNCT_1:21;
then A52: (q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))) /. i = (q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))) . i by PARTFUN1:def 8
.= q . ((Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) . i) by A51, FUNCT_1:22
.= q . ((Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) /. i) by A50, PARTFUN1:def 8
.= q . ((SgmX ((BagOrder n),(Support p))) /. i) by A48, FINSEQ_5:75
.= p . ((SgmX ((BagOrder n),(Support p))) /. i) by A3, A41
.= p . ((SgmX ((BagOrder n),(Support p))) . i) by A40, PARTFUN1:def 8
.= (p * (SgmX ((BagOrder n),(Support p)))) . i by A49, FUNCT_1:22
.= (p * (SgmX ((BagOrder n),(Support p)))) /. i by A49, PARTFUN1:def 8 ;
A53: yq /. i = ((q * (SgmX ((BagOrder n),(Support q)))) /. i) * (eval ((((SgmX ((BagOrder n),(Support q))) /. i) @),x)) by A17, A22, A23, A50
.= ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval ((((SgmX ((BagOrder n),(Support p))) /. i) @),x)) by A11, A48, A52, FINSEQ_5:75
.= yp /. i by A14, A22, A50, A42
.= (Ins (yp,k9,((q . b) * (eval (b,x))))) /. i by A37, FINSEQ_5:75 ;
thus yq . i = yq /. i by A24, PARTFUN1:def 8
.= (Ins (yp,k9,((q . b) * (eval (b,x))))) . i by A25, A53, PARTFUN1:def 8 ; :: thesis: verum

end;

case A54: i > k ; :: thesis: yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i

then i - 1 > k9 by XREAL_1:11;
then reconsider i1 = i - 1 as Element of NAT by INT_1:16;
A55: (i - 1) + 1 = i + 0 ;
then A56: k9 + 1 <= i1 by A54, NAT_1:13;
A57: dom q = Bags n by FUNCT_2:def 1;
A58: rng (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) c= Bags n by FINSEQ_1:def 4;
A59: dom p = Bags n by FUNCT_2:def 1;
A60: rng (SgmX ((BagOrder n),(Support p))) c= Bags n by FINSEQ_1:def 4;
A61: i - 1 <= ((len yp) + 1) - 1 by A15, A12, A18, A23, XREAL_1:11;
0 + 1 <= k9 + 1 by XREAL_1:8;
then 1 < i by A54, XXREAL_0:2;
then A62: 1 <= i1 by A55, NAT_1:13;
then i1 in Seg (len (SgmX ((BagOrder n),(Support p)))) by A12, A61, FINSEQ_1:3;
then A63: i1 in dom (SgmX ((BagOrder n),(Support p))) by FINSEQ_1:def 3;

A64: now

assume (SgmX ((BagOrder n),(Support p))) /. i1 = b ; :: thesis: contradiction
then (SgmX ((BagOrder n),(Support p))) . i1 = b by A63, PARTFUN1:def 8;
then b in rng (SgmX ((BagOrder n),(Support p))) by A63, FUNCT_1:def 5;
hence contradiction by A1, A20, PRE_POLY:def 2; :: thesis: verum

end;

(SgmX ((BagOrder n),(Support p))) . i1 in rng (SgmX ((BagOrder n),(Support p))) by A63, FUNCT_1:def 5;
then A65: i1 in dom (p * (SgmX ((BagOrder n),(Support p)))) by A63, A60, A59, FUNCT_1:21;
A67: i = i1 + 1 ;
A68: i in dom (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) by A15, A18, A22, A23, A32, FINSEQ_1:3;
then (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) . i in rng (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) by FUNCT_1:def 5;
then A69: i in dom (q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))) by A68, A58, A57, FUNCT_1:21;
then A70: (q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))) /. i = (q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))) . i by PARTFUN1:def 8
.= q . ((Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) . i) by A69, FUNCT_1:22
.= q . ((Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) /. i) by A68, PARTFUN1:def 8
.= q . ((SgmX ((BagOrder n),(Support p))) /. i1) by A12, A61, A67, A56, FINSEQ_5:77
.= p . ((SgmX ((BagOrder n),(Support p))) /. i1) by A3, A64
.= p . ((SgmX ((BagOrder n),(Support p))) . i1) by A63, PARTFUN1:def 8
.= (p * (SgmX ((BagOrder n),(Support p)))) . i1 by A65, FUNCT_1:22
.= (p * (SgmX ((BagOrder n),(Support p)))) /. i1 by A65, PARTFUN1:def 8 ;
A71: yq /. i = ((q * (SgmX ((BagOrder n),(Support q)))) /. i) * (eval ((((SgmX ((BagOrder n),(Support q))) /. i) @),x)) by A17, A22, A23, A68
.= ((p * (SgmX ((BagOrder n),(Support p)))) /. i1) * (eval ((((SgmX ((BagOrder n),(Support p))) /. i1) @),x)) by A11, A12, A61, A67, A56, A70, FINSEQ_5:77
.= yp /. i1 by A14, A61, A62
.= (Ins (yp,k9,((q . b) * (eval (b,x))))) /. i by A61, A67, A56, FINSEQ_5:77 ;
thus yq . i = yq /. i by A24, PARTFUN1:def 8
.= (Ins (yp,k9,((q . b) * (eval (b,x))))) . i by A25, A71, PARTFUN1:def 8 ; :: thesis: verum

end;

end;

end;

hence yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i ; :: thesis: verum

end;

end;

end;

Sum (((yp | k9) ^ <*((q . b) * (eval (b,x)))*>) ^ (yp /^ k9)) = (Sum ((yp | k9) ^ <*((q . b) * (eval (b,x)))*>)) + (Sum (yp /^ k9)) by RLVECT_1:58
.= ((Sum (yp | k9)) + (Sum <*((q . b) * (eval (b,x)))*>)) + (Sum (yp /^ k9)) by RLVECT_1:58
.= ((Sum (yp | k9)) + (Sum (yp /^ k9))) + (Sum <*((q . b) * (eval (b,x)))*>) by RLVECT_1:def 6
.= (Sum ((yp | k9) ^ (yp /^ k9))) + (Sum <*((q . b) * (eval (b,x)))*>) by RLVECT_1:58
.= (Sum yp) + (Sum <*((q . b) * (eval (b,x)))*>) by RFINSEQ:21
.= (eval (p,x)) + ((q . b) * (eval (b,x))) by A13, RLVECT_1:61 ;
then Sum (Ins (yp,k9,((q . b) * (eval (b,x))))) = (eval (p,x)) + ((q . b) * (eval (b,x))) by FINSEQ_5:def 4;
hence eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x))) by A16, A19, A21, FINSEQ_1:18; :: thesis: verum