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