let n be Ordinal; :: thesis: for R, S being non degenerated comRing
for p, q being Polynomial of n,R
for x being Function of n,S
for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b1 being bag of n st b1 <> b holds
q . b1 = p . b1 ) holds
Ext_eval (q,x) = (Ext_eval (p,x)) + ((In ((q . b),S)) * (eval (b,x)))
let R, S be non degenerated comRing; :: thesis: for p, q being Polynomial of n,R
for x being Function of n,S
for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b1 being bag of n st b1 <> b holds
q . b1 = p . b1 ) holds
Ext_eval (q,x) = (Ext_eval (p,x)) + ((In ((q . b),S)) * (eval (b,x)))
let p, q be Polynomial of n,R; :: thesis: for x being Function of n,S
for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b1 being bag of n st b1 <> b holds
q . b1 = p . b1 ) holds
Ext_eval (q,x) = (Ext_eval (p,x)) + ((In ((q . b),S)) * (eval (b,x)))
let x be Function of n,S; :: thesis: for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b1 being bag of n st b1 <> b holds
q . b1 = p . b1 ) holds
Ext_eval (q,x) = (Ext_eval (p,x)) + ((In ((q . b),S)) * (eval (b,x)))
let b be bag of n; :: thesis: ( not b in Support p & Support q = (Support p) \/ {b} & ( for b1 being bag of n st b1 <> b holds
q . b1 = p . b1 ) implies Ext_eval (q,x) = (Ext_eval (p,x)) + ((In ((q . b),S)) * (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: Ext_eval (q,x) = (Ext_eval (p,x)) + ((In ((q . b),S)) * (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 POLYNOM2:18;
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:10;
A7: (SgmX ((BagOrder n),(Support q))) /. k = b by A5, A6, PARTFUN1:def 6;
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:1;
1 <= k by A5, A8, FINSEQ_1:1;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
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, POLYNOM2:18, PRE_POLY:80;
consider yp being FinSequence of S such that
A13: Ext_eval (p,x) = Sum yp and
A12: len yp = len (SgmX ((BagOrder n),(Support p))) and
A14: for i being Element of NAT st 1 <= i & i <= len yp holds
yp . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) by defeval;
consider yq being FinSequence of S such that
A16: Ext_eval (q,x) = Sum yq and
A15: len yq = len (SgmX ((BagOrder n),(Support q))) and
A17: for i being Element of NAT st 1 <= i & i <= len yq holds
yq . i = (In (((q * (SgmX ((BagOrder n),(Support q)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support q))) /. i),x)) by defeval;
VA: dom yq = dom (SgmX ((BagOrder n),(Support q))) by A15, FINSEQ_3:29;
reconsider b = b as Element of Bags n ;
set ytmp = Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))));
A18: (len (SgmX ((BagOrder n),(Support p)))) + 1 = (card (Support p)) + 1 by POLYNOM2:18, PRE_POLY:11
.= card (Support q) by A1, A2, CARD_2:41
.= len (SgmX ((BagOrder n),(Support q))) by POLYNOM2:18, PRE_POLY:11 ;
then A19: len yq = len (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) by A15, A12, FINSEQ_5:69;
A20: BagOrder n linearly_orders Support p by POLYNOM2:18;
A21: for i being Nat st 1 <= i & i <= len yq holds
yq . i = (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len yq implies yq . i = (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) . i )
assume that
A22: 1 <= i and
A23: i <= len yq ; :: thesis: yq . i = (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) . i
i in Seg (len (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x)))))) by A19, A22, A23;
then A25: i in dom (Ins (yp,k9,((In ((q . b),S)) * (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,((In ((q . b),S)) * (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 k in dom (q * (SgmX ((BagOrder n),(Support q)))) by A5, FUNCT_1:11;
then A28: (q * (SgmX ((BagOrder n),(Support q)))) . k = q . b by A6, FUNCT_1:12;
A29: yq . i = (In (((q * (SgmX ((BagOrder n),(Support q)))) . k),S)) * (eval (((SgmX ((BagOrder n),(Support q))) /. k),x)) by A5, A17, A22, A23, A26
.= (In ((q . b),S)) * (eval (b,x)) by A5, A6, A28, PARTFUN1:def 6 ;
A30: k9 <= len yp by A8, A10, A12, A18, A5, FINSEQ_1:1, XREAL_1:6;
thus (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) . i = yq . i by A29, A10, A26, A30, FINSEQ_5:73; :: thesis: verum

end;

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

len (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) = (len (SgmX ((BagOrder n),(Support p)))) + 1 by FINSEQ_5:69;
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 :: thesis: ( ( i < k & yq . i = (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) . i ) or ( i > k & yq . i = (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) . i ) )

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

case A33: i < k ; :: thesis: yq . i = (Ins (yp,k9,((In ((q . b),S)) * (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;
A36: i <= k9 by A10, A33, NAT_1:13;
then i in Seg k9 by A22;
then A37: i in dom (yp | k9) by A34, FINSEQ_1:17;
A38: k - 1 <= ((len (SgmX ((BagOrder n),(Support p)))) + 1) - 1 by A9, A18, XREAL_1:9;
then A39: i <= len (SgmX ((BagOrder n),(Support p))) by A36, XXREAL_0:2;
then A40: i in dom (SgmX ((BagOrder n),(Support p))) by A22, FINSEQ_3:25;

A41: now :: thesis: not (SgmX ((BagOrder n),(Support p))) /. i = b

assume (SgmX ((BagOrder n),(Support p))) /. i = b ; :: thesis: contradiction
then (SgmX ((BagOrder n),(Support p))) . i = b by A40, PARTFUN1:def 6;
then b in rng (SgmX ((BagOrder n),(Support p))) by A40, FUNCT_1:def 3;
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;
A44: rng (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) c= Bags n by FINSEQ_1:def 4;
A45: dom q = Bags n by FUNCT_2:def 1;
A46: rng (SgmX ((BagOrder n),(Support p))) c= Bags n by FINSEQ_1:def 4;
i in Seg k9 by A22, A36;
then A47: i in dom ((SgmX ((BagOrder n),(Support p))) | k9) by A38, FINSEQ_1:17;
(SgmX ((BagOrder n),(Support p))) . i in rng (SgmX ((BagOrder n),(Support p))) by A40, FUNCT_1:def 3;
then (SgmX ((BagOrder n),(Support p))) . i in Bags n by A46;
then (SgmX ((BagOrder n),(Support p))) . i in dom p by FUNCT_2:def 1;
then A48: i in dom (p * (SgmX ((BagOrder n),(Support p)))) by A40, FUNCT_1:11;
len (SgmX ((BagOrder n),(Support p))) <= (len (SgmX ((BagOrder n),(Support p)))) + 1 by XREAL_1:29;
then i <= (len (SgmX ((BagOrder n),(Support p)))) + 1 by A39, XXREAL_0:2;
then A49: i in dom (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) by A22, A32;
then (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) . i in rng (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) by FUNCT_1:def 3;
then i in dom (q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))) by A49, A44, A45, FUNCT_1:11;
then A51: (q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))) . i = q . ((Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) . i) by FUNCT_1:12
.= q . ((SgmX ((BagOrder n),(Support p))) . i) by A47, FINSEQ_5:72
.= q . ((SgmX ((BagOrder n),(Support p))) /. i) by A40, PARTFUN1:def 6
.= p . ((SgmX ((BagOrder n),(Support p))) /. i) by A3, A41
.= p . ((SgmX ((BagOrder n),(Support p))) . i) by A40, PARTFUN1:def 6
.= (p * (SgmX ((BagOrder n),(Support p)))) . i by A48, FUNCT_1:12 ;
Z1: ( (SgmX ((BagOrder n),(Support q))) /. i = (SgmX ((BagOrder n),(Support q))) . i & (SgmX ((BagOrder n),(Support p))) /. i = (SgmX ((BagOrder n),(Support p))) . i ) by VA, A22, A23, FINSEQ_3:25, A40, PARTFUN1:def 6;
A52: yq . i = (In (((q * (SgmX ((BagOrder n),(Support q)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support q))) /. i),x)) by A17, A22, A23, A49
.= (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) by A11, A47, A51, FINSEQ_5:72, Z1
.= yp . i by A14, A22, A49, A42
.= (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) . i by A37, FINSEQ_5:72
.= (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) /. i by A25, PARTFUN1:def 6 ;
thus yq . i = (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) . i by A25, A52, PARTFUN1:def 6; :: thesis: verum

end;

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

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

A63: now :: thesis: not (SgmX ((BagOrder n),(Support p))) /. i1 = b

assume (SgmX ((BagOrder n),(Support p))) /. i1 = b ; :: thesis: contradiction
then (SgmX ((BagOrder n),(Support p))) . i1 = b by A62, PARTFUN1:def 6;
then b in rng (SgmX ((BagOrder n),(Support p))) by A62, FUNCT_1:def 3;
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 A62, FUNCT_1:def 3;
then A64: i1 in dom (p * (SgmX ((BagOrder n),(Support p)))) by A62, A59, A58, FUNCT_1:11;
A65: i = i1 + 1 ;
A66: i in dom (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) by A15, A18, A22, A23, A32;
then (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) . i in rng (Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) by FUNCT_1:def 3;
then i in dom (q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))) by A66, A57, A56, FUNCT_1:11;
then A68: (q * (Ins ((SgmX ((BagOrder n),(Support p))),k9,b))) . i = q . ((Ins ((SgmX ((BagOrder n),(Support p))),k9,b)) . i) by FUNCT_1:12
.= q . ((SgmX ((BagOrder n),(Support p))) . i1) by A12, A60, A65, A55, FINSEQ_5:74
.= q . ((SgmX ((BagOrder n),(Support p))) /. i1) by A62, PARTFUN1:def 6
.= p . ((SgmX ((BagOrder n),(Support p))) /. i1) by A3, A63
.= p . ((SgmX ((BagOrder n),(Support p))) . i1) by A62, PARTFUN1:def 6
.= (p * (SgmX ((BagOrder n),(Support p)))) . i1 by A64, FUNCT_1:12 ;
dom yq = dom (SgmX ((BagOrder n),(Support q))) by FINSEQ_3:29, A15;
then BB: (SgmX ((BagOrder n),(Support q))) /. i = (SgmX ((BagOrder n),(Support q))) . i by A22, A23, FINSEQ_3:25, PARTFUN1:def 6
.= (SgmX ((BagOrder n),(Support p))) . i1 by A12, A60, A65, A55, A11, FINSEQ_5:74
.= (SgmX ((BagOrder n),(Support p))) /. i1 by PARTFUN1:def 6, A62 ;
A69: yq . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i1),S)) * (eval (((SgmX ((BagOrder n),(Support q))) /. i),x)) by A68, A11, A17, A22, A23, A66
.= yp . i1 by A14, A60, A61, BB
.= (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) . i by A60, A65, A55, FINSEQ_5:74
.= (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) /. i by PARTFUN1:def 6, A25 ;
thus yq . i = (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) . i by A25, A69, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

Sum (((yp | k9) ^ <*((In ((q . b),S)) * (eval (b,x)))*>) ^ (yp /^ k9)) = (Sum ((yp | k9) ^ <*((In ((q . b),S)) * (eval (b,x)))*>)) + (Sum (yp /^ k9)) by RLVECT_1:41
.= ((Sum (yp | k9)) + (Sum <*((In ((q . b),S)) * (eval (b,x)))*>)) + (Sum (yp /^ k9)) by RLVECT_1:41
.= ((Sum (yp | k9)) + (Sum (yp /^ k9))) + (Sum <*((In ((q . b),S)) * (eval (b,x)))*>) by RLVECT_1:def 3
.= (Sum ((yp | k9) ^ (yp /^ k9))) + (Sum <*((In ((q . b),S)) * (eval (b,x)))*>) by RLVECT_1:41
.= (Sum yp) + (Sum <*((In ((q . b),S)) * (eval (b,x)))*>) by RFINSEQ:8
.= (Ext_eval (p,x)) + ((In ((q . b),S)) * (eval (b,x))) by A13, RLVECT_1:44 ;
then Sum (Ins (yp,k9,((In ((q . b),S)) * (eval (b,x))))) = (Ext_eval (p,x)) + ((In ((q . b),S)) * (eval (b,x))) by FINSEQ_5:def 4;
hence Ext_eval (q,x) = (Ext_eval (p,x)) + ((In ((q . b),S)) * (eval (b,x))) by A16, A19, A21, FINSEQ_1:14; :: thesis: verum