let n be Ordinal; :: thesis: for L being 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 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 Th10;
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 1 - 1 <= k - 1 by XREAL_1:9;
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, Th10, PRE_POLY:80;
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 Def2;
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 Def2;
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,((q . b) * (eval (b,x))));
A18: (len (SgmX ((BagOrder n),(Support p)))) + 1 = (card (Support p)) + 1 by Th10, PRE_POLY:11
.= card (Support q) by A1, A2, CARD_2:41
.= len (SgmX ((BagOrder n),(Support q))) by Th10, PRE_POLY:11 ;
then A19: len yq = len (Ins (yp,k9,((q . b) * (eval (b,x))))) by A15, A12, FINSEQ_5:69;
A20: BagOrder n linearly_orders Support p by Th10;
A21: for i being Nat st 1 <= i & i <= len yq holds
yq . i = (Ins (yp,k9,((q . b) * (eval (b,x))))) . i Sum (((yp | k9) ^ <*((q . b) * (eval (b,x)))*>) ^ (yp /^ k9)) = (Sum ((yp | k9) ^ <*((q . b) * (eval (b,x)))*>)) + (Sum (yp /^ k9)) by RLVECT_1:41
.= ((Sum (yp | k9)) + (Sum <*((q . b) * (eval (b,x)))*>)) + (Sum (yp /^ k9)) by RLVECT_1:41
.= ((Sum (yp | k9)) + (Sum (yp /^ k9))) + (Sum <*((q . b) * (eval (b,x)))*>) by RLVECT_1:def 3
.= (Sum ((yp | k9) ^ (yp /^ k9))) + (Sum <*((q . b) * (eval (b,x)))*>) by RLVECT_1:41
.= (Sum yp) + (Sum <*((q . b) * (eval (b,x)))*>) by RFINSEQ:8
.= (eval (p,x)) + ((q . b) * (eval (b,x))) by A13, RLVECT_1:44 ;
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:14; :: thesis: verum