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 st not b in Support p & Support q = (Support p) \/ {b} & ( for b' being bag of st b' <> b holds
q . b' = p . b' ) 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 st not b in Support p & Support q = (Support p) \/ {b} & ( for b' being bag of st b' <> b holds
q . b' = p . b' ) 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 st not b in Support p & Support q = (Support p) \/ {b} & ( for b' being bag of st b' <> b holds
q . b' = p . b' ) 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 st not b in Support p & Support q = (Support p) \/ {b} & ( for b' being bag of st b' <> b holds
q . b' = p . b' ) holds
eval q,x = (eval p,x) + ((q . b) * (eval b,x))
let b be bag of ; :: thesis: ( not b in Support p & Support q = (Support p) \/ {b} & ( for b' being bag of st b' <> b holds
q . b' = p . b' ) implies eval q,x = (eval p,x) + ((q . b) * (eval b,x)) )
assume A1: ( not b in Support p & Support q = (Support p) \/ {b} & ( for b' being bag of st b' <> b holds
q . b' = p . b' ) ) ; :: 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);
A2: ( BagOrder n linearly_orders Support q & BagOrder n linearly_orders Support p ) by Th20;
b in {b} by TARSKI:def 1;
then b in Support q by A1, XBOOLE_0:def 3;
then b in rng (SgmX (BagOrder n),(Support q)) by A2, TRIANG_1:def 2;
then consider k being Nat such that
A3: ( k in dom (SgmX (BagOrder n),(Support q)) & (SgmX (BagOrder n),(Support q)) . k = b ) by FINSEQ_2:11;
A4: (SgmX (BagOrder n),(Support q)) /. k = b by A3, PARTFUN1:def 8;
dom (SgmX (BagOrder n),(Support q)) = Seg (len (SgmX (BagOrder n),(Support q))) by FINSEQ_1:def 3;
then A5: ( 1 <= k & k <= len (SgmX (BagOrder n),(Support q)) ) by A3, FINSEQ_1:3;
then 1 - 1 <= k - 1 by XREAL_1:11;
then reconsider k' = k - 1 as Element of NAT by INT_1:16;
reconsider b = b as Element of Bags n by POLYNOM1:def 14;
A6: k' + 1 = k + 0 ;
then A7: SgmX (BagOrder n),(Support q) = Ins (SgmX (BagOrder n),(Support p)),k',b by A1, A2, A3, A4, Th13;
consider yq being FinSequence of the carrier of L such that
A8: ( len yq = len (SgmX (BagOrder n),(Support q)) & Sum yq = eval q,x & ( 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;
consider yp being FinSequence of the carrier of L such that
A9: ( len yp = len (SgmX (BagOrder n),(Support p)) & Sum yp = eval p,x & ( 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;
reconsider b = b as Element of Bags n ;
set ytmp = Ins yp,k',((q . b) * (eval b,x));
Sum (((yp | k') ^ <*((q . b) * (eval b,x))*>) ^ (yp /^ k')) = (Sum ((yp | k') ^ <*((q . b) * (eval b,x))*>)) + (Sum (yp /^ k')) by RLVECT_1:58
.= ((Sum (yp | k')) + (Sum <*((q . b) * (eval b,x))*>)) + (Sum (yp /^ k')) by RLVECT_1:58
.= ((Sum (yp | k')) + (Sum (yp /^ k'))) + (Sum <*((q . b) * (eval b,x))*>) by RLVECT_1:def 6
.= (Sum ((yp | k') ^ (yp /^ k'))) + (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 A9, RLVECT_1:61 ;
then A10: Sum (Ins yp,k',((q . b) * (eval b,x))) = (eval p,x) + ((q . b) * (eval b,x)) by FINSEQ_5:def 4;
A11: (len (SgmX (BagOrder n),(Support p))) + 1 = (card (Support p)) + 1 by Th20, TRIANG_1:9
.= card (Support q) by A1, CARD_2:54
.= len (SgmX (BagOrder n),(Support q)) by Th20, TRIANG_1:9 ;
then A12: len yq = len (Ins yp,k',((q . b) * (eval b,x))) by A8, A9, FINSEQ_5:72;
for i being Nat st 1 <= i & i <= len yq holds
yq . i = (Ins yp,k',((q . b) * (eval b,x))) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len yq implies yq . i = (Ins yp,k',((q . b) * (eval b,x))) . i )
assume A13: ( 1 <= i & i <= len yq ) ; :: thesis: yq . i = (Ins yp,k',((q . b) * (eval b,x))) . i
then ( i in Seg (len yq) & i in Seg (len (Ins yp,k',((q . b) * (eval b,x)))) ) by A12, FINSEQ_1:3;
then A14: ( i in dom yq & i in dom (Ins yp,k',((q . b) * (eval b,x))) ) by FINSEQ_1:def 3;

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

suppose A15: i = k ; :: thesis: yq . i = (Ins yp,k',((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 A3, POLYNOM1:def 14;
then A16: k in dom (q * (SgmX (BagOrder n),(Support q))) by A3, FUNCT_1:21;
then A17: (q * (SgmX (BagOrder n),(Support q))) /. k = (q * (SgmX (BagOrder n),(Support q))) . k by PARTFUN1:def 8
.= q . b by A3, A16, FUNCT_1:22 ;
A18: yq /. i = ((q * (SgmX (BagOrder n),(Support q))) /. k) * (eval (((SgmX (BagOrder n),(Support q)) /. k) @ ),x) by A3, A8, A13, A15
.= (q . b) * (eval b,x) by A3, A17, PARTFUN1:def 8 ;
A19: k' <= len yp by A5, A6, A9, A11, XREAL_1:8;
thus (Ins yp,k',((q . b) * (eval b,x))) . i = (Ins yp,k',((q . b) * (eval b,x))) /. i by A14, PARTFUN1:def 8
.= (q . b) * (eval b,x) by A6, A15, A19, FINSEQ_5:76
.= yq . i by A14, A18, PARTFUN1:def 8 ; :: thesis: verum

end;

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

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

now

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

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

then A23: i <= k' by A6, NAT_1:13;
then A24: i in Seg k' by A13, FINSEQ_1:3;
A25: k - 1 <= ((len (SgmX (BagOrder n),(Support p))) + 1) - 1 by A5, A11, XREAL_1:11;
then A26: i <= len (SgmX (BagOrder n),(Support p)) by A23, XXREAL_0:2;
(SgmX (BagOrder n),(Support p)) | (Seg k') is FinSequence by FINSEQ_1:19;
then i in dom ((SgmX (BagOrder n),(Support p)) | (Seg k')) by A24, A25, FINSEQ_1:21;
then A27: i in dom ((SgmX (BagOrder n),(Support p)) | k') by FINSEQ_1:def 15;
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 A26, XXREAL_0:2;
then A28: i in dom (Ins (SgmX (BagOrder n),(Support p)),k',b) by A13, A21, FINSEQ_1:3;
then A29: (Ins (SgmX (BagOrder n),(Support p)),k',b) . i in rng (Ins (SgmX (BagOrder n),(Support p)),k',b) by FUNCT_1:def 5;
A30: rng (Ins (SgmX (BagOrder n),(Support p)),k',b) c= Bags n by FINSEQ_1:def 4;
A31: (SgmX (BagOrder n),(Support p)) /. i is bag of by POLYNOM1:def 14;
i in Seg (len (SgmX (BagOrder n),(Support p))) by A13, A26, FINSEQ_1:3;
then A32: i in dom (SgmX (BagOrder n),(Support p)) by FINSEQ_1:def 3;
then A33: (SgmX (BagOrder n),(Support p)) . i in rng (SgmX (BagOrder n),(Support p)) by FUNCT_1:def 5;
rng (SgmX (BagOrder n),(Support p)) c= Bags n by FINSEQ_1:def 4;
then (SgmX (BagOrder n),(Support p)) . i in Bags n by A33;
then (SgmX (BagOrder n),(Support p)) . i in dom p by FUNCT_2:def 1;
then A34: i in dom (p * (SgmX (BagOrder n),(Support p))) by A32, FUNCT_1:21;

A35: now

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

end;

k' < k by A6, NAT_1:19;
then k' < len yq by A5, A8, XXREAL_0:2;
then A36: k' <= len yp by A8, A9, A11, NAT_1:13;
i < len yq by A5, A8, A22, XXREAL_0:2;
then A37: i <= len yp by A8, A9, A11, NAT_1:13;
A38: i in Seg k' by A13, A23, FINSEQ_1:3;
yp | (Seg k') is FinSequence by FINSEQ_1:19;
then i in dom (yp | (Seg k')) by A36, A38, FINSEQ_1:21;
then A39: i in dom (yp | k') by FINSEQ_1:def 15;
dom q = Bags n by FUNCT_2:def 1;
then A40: i in dom (q * (Ins (SgmX (BagOrder n),(Support p)),k',b)) by A28, A29, A30, FUNCT_1:21;
then A41: (q * (Ins (SgmX (BagOrder n),(Support p)),k',b)) /. i = (q * (Ins (SgmX (BagOrder n),(Support p)),k',b)) . i by PARTFUN1:def 8
.= q . ((Ins (SgmX (BagOrder n),(Support p)),k',b) . i) by A40, FUNCT_1:22
.= q . ((Ins (SgmX (BagOrder n),(Support p)),k',b) /. i) by A28, PARTFUN1:def 8
.= q . ((SgmX (BagOrder n),(Support p)) /. i) by A27, FINSEQ_5:75
.= p . ((SgmX (BagOrder n),(Support p)) /. i) by A1, A31, A35
.= p . ((SgmX (BagOrder n),(Support p)) . i) by A32, PARTFUN1:def 8
.= (p * (SgmX (BagOrder n),(Support p))) . i by A34, FUNCT_1:22
.= (p * (SgmX (BagOrder n),(Support p))) /. i by A34, PARTFUN1:def 8 ;
A42: yq /. i = ((q * (SgmX (BagOrder n),(Support q))) /. i) * (eval (((SgmX (BagOrder n),(Support q)) /. i) @ ),x) by A8, A13, A28
.= ((p * (SgmX (BagOrder n),(Support p))) /. i) * (eval (((SgmX (BagOrder n),(Support p)) /. i) @ ),x) by A7, A27, A41, FINSEQ_5:75
.= yp /. i by A9, A13, A28, A37
.= (Ins yp,k',((q . b) * (eval b,x))) /. i by A39, FINSEQ_5:75 ;
thus yq . i = yq /. i by A14, PARTFUN1:def 8
.= (Ins yp,k',((q . b) * (eval b,x))) . i by A14, A42, PARTFUN1:def 8 ; :: thesis: verum

end;

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

then i - 1 > k' by XREAL_1:11;
then reconsider i1 = i - 1 as Element of NAT by INT_1:16;
A44: (i - 1) + 1 = i + 0 ;
A45: i - 1 <= ((len yp) + 1) - 1 by A8, A9, A11, A13, XREAL_1:11;
0 + 1 <= k' + 1 by XREAL_1:8;
then 1 < i by A43, XXREAL_0:2;
then A46: 1 <= i1 by A44, NAT_1:13;
then i1 in Seg (len (SgmX (BagOrder n),(Support p))) by A9, A45, FINSEQ_1:3;
then A47: i1 in dom (SgmX (BagOrder n),(Support p)) by FINSEQ_1:def 3;
A48: (SgmX (BagOrder n),(Support p)) /. i1 is bag of by POLYNOM1:def 14;

A49: now

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

end;

A50: (SgmX (BagOrder n),(Support p)) . i1 in rng (SgmX (BagOrder n),(Support p)) by A47, FUNCT_1:def 5;
A51: rng (SgmX (BagOrder n),(Support p)) c= Bags n by FINSEQ_1:def 4;
dom p = Bags n by FUNCT_2:def 1;
then A52: i1 in dom (p * (SgmX (BagOrder n),(Support p))) by A47, A50, A51, FUNCT_1:21;
A53: i in dom (Ins (SgmX (BagOrder n),(Support p)),k',b) by A8, A11, A13, A21, FINSEQ_1:3;
then A54: (Ins (SgmX (BagOrder n),(Support p)),k',b) . i in rng (Ins (SgmX (BagOrder n),(Support p)),k',b) by FUNCT_1:def 5;
A55: rng (Ins (SgmX (BagOrder n),(Support p)),k',b) c= Bags n by FINSEQ_1:def 4;
A56: i = i1 + 1 ;
A57: k' + 1 <= i1 by A43, A44, NAT_1:13;
dom q = Bags n by FUNCT_2:def 1;
then A58: i in dom (q * (Ins (SgmX (BagOrder n),(Support p)),k',b)) by A53, A54, A55, FUNCT_1:21;
then A59: (q * (Ins (SgmX (BagOrder n),(Support p)),k',b)) /. i = (q * (Ins (SgmX (BagOrder n),(Support p)),k',b)) . i by PARTFUN1:def 8
.= q . ((Ins (SgmX (BagOrder n),(Support p)),k',b) . i) by A58, FUNCT_1:22
.= q . ((Ins (SgmX (BagOrder n),(Support p)),k',b) /. i) by A53, PARTFUN1:def 8
.= q . ((SgmX (BagOrder n),(Support p)) /. i1) by A9, A45, A56, A57, FINSEQ_5:77
.= p . ((SgmX (BagOrder n),(Support p)) /. i1) by A1, A48, A49
.= p . ((SgmX (BagOrder n),(Support p)) . i1) by A47, PARTFUN1:def 8
.= (p * (SgmX (BagOrder n),(Support p))) . i1 by A52, FUNCT_1:22
.= (p * (SgmX (BagOrder n),(Support p))) /. i1 by A52, PARTFUN1:def 8 ;
A60: yq /. i = ((q * (SgmX (BagOrder n),(Support q))) /. i) * (eval (((SgmX (BagOrder n),(Support q)) /. i) @ ),x) by A8, A13, A53
.= ((p * (SgmX (BagOrder n),(Support p))) /. i1) * (eval (((SgmX (BagOrder n),(Support p)) /. i1) @ ),x) by A7, A9, A45, A56, A57, A59, FINSEQ_5:77
.= yp /. i1 by A9, A45, A46
.= (Ins yp,k',((q . b) * (eval b,x))) /. i by A45, A56, A57, FINSEQ_5:77 ;
thus yq . i = yq /. i by A14, PARTFUN1:def 8
.= (Ins yp,k',((q . b) * (eval b,x))) . i by A14, A60, PARTFUN1:def 8 ; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

hence eval q,x = (eval p,x) + ((q . b) * (eval b,x)) by A8, A10, A12, FINSEQ_1:18; :: thesis: verum