let O be Ordinal; :: thesis:
let R be non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis:
let t be bag of O; :: thesis:
let p be Polynomial of O,R; :: thesis:
let i be object ; :: thesis:
let x be Function of O,R; :: thesis:
assume A1: i in O ; :: thesis:
set xE = x +* (i,(eval (p,x)));
set P = p `^ (t . i);
set t0 = t +* (i,0);
set SS = SgmX ((BagOrder O),(Support (p `^ (t . i))));
set Smp = Subst (t,i,p);
consider y being FinSequence of R such that
A2: ( len y = len (SgmX ((BagOrder O),(Support (p `^ (t . i))))) & eval ((p `^ (t . i)),x) = Sum y ) and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (((p `^ (t . i)) * (SgmX ((BagOrder O),(Support (p `^ (t . i)))))) /. i) * (eval (((SgmX ((BagOrder O),(Support (p `^ (t . i))))) /. i),x)) by POLYNOM2:def 4;
BagOrder O linearly_orders Support (p `^ (t . i)) by POLYNOM2:18;
then A4: rng (SgmX ((BagOrder O),(Support (p `^ (t . i))))) = Support (p `^ (t . i)) by PRE_POLY:def 2;
A5: SgmX ((BagOrder O),(Support (p `^ (t . i)))) is one-to-one by POLYNOM2:18, PRE_POLY:10;
consider tran being one-to-one FinSequence of Bags O such that
A6: rng tran = Support (Subst (t,i,p)) and
A7: len tran = len (SgmX ((BagOrder O),(Support (p `^ (t . i))))) and
A8: for j being Nat st 1 <= j & j <= len tran holds
tran . j = Subst (t,i,((SgmX ((BagOrder O),(Support (p `^ (t . i))))) /. j)) by A4, A5, Th34;
A9: len tran = card (Support (Subst (t,i,p))) by A6, FINSEQ_4:62;
A10: card (Support (Subst (t,i,p))) = len (SgmX ((BagOrder O),(Support (p `^ (t . i))))) by A6, FINSEQ_4:62, A7;
consider Y being FinSequence of R such that
A11: ( len Y = card (Support (Subst (t,i,p))) & eval ((Subst (t,i,p)),x) = Sum Y ) and
A12: for i being Nat st 1 <= i & i <= len Y holds
Y /. i = (((Subst (t,i,p)) * tran) /. i) * (eval ((tran /. i),x)) by A6, HILB10_2:24;
A13: dom (y * (eval ((t +* (i,0)),x))) = dom y by POLYNOM1:def 2;
then A14: len (y * (eval ((t +* (i,0)),x))) = len y by FINSEQ_3:29;
A15: eval ((p `^ (t . i)),x) = (power R) . ((eval (p,x)),(t . i)) by Th30;
for j being Nat st 1 <= j & j <= len Y holds
Y . j = (y * (eval ((t +* (i,0)),x))) . j

proof

let j be Nat; :: thesis:
assume A16: ( 1 <= j & j <= len Y ) ; :: thesis:
A17: j in NAT by ORDINAL1:def 12;
A18: ( len Y = len tran & len tran = len (SgmX ((BagOrder O),(Support (p `^ (t . i))))) & len (SgmX ((BagOrder O),(Support (p `^ (t . i))))) = len y ) by A2, A11, A6, FINSEQ_4:62, A7;
A19: rng tran c= Bags O by RELAT_1:def 19;
( dom (p `^ (t . i)) = Bags O & Bags O = dom (Subst (t,i,p)) ) by FUNCT_2:def 1;
then A20: ( dom ((p `^ (t . i)) * (SgmX ((BagOrder O),(Support (p `^ (t . i)))))) = dom (SgmX ((BagOrder O),(Support (p `^ (t . i))))) & dom ((Subst (t,i,p)) * tran) = dom tran ) by A19, A4, RELAT_1:27;
A21: ( j in dom tran & j in dom (SgmX ((BagOrder O),(Support (p `^ (t . i))))) & j in dom y & j in dom Y ) by A16, A2, A11, A7, A9, FINSEQ_3:25;
then A22: ( tran /. j = tran . j & tran . j = Subst (t,i,((SgmX ((BagOrder O),(Support (p `^ (t . i))))) /. j)) ) by A16, A8, A11, A9, PARTFUN1:def 6;
A23: ((p `^ (t . i)) * (SgmX ((BagOrder O),(Support (p `^ (t . i)))))) /. j = ((p `^ (t . i)) * (SgmX ((BagOrder O),(Support (p `^ (t . i)))))) . j by A20, A16, A11, A10, FINSEQ_3:25, PARTFUN1:def 6
.= (p `^ (t . i)) . ((SgmX ((BagOrder O),(Support (p `^ (t . i))))) . j) by A20, A16, A11, A10, FINSEQ_3:25, FUNCT_1:12
.= (p `^ (t . i)) . ((SgmX ((BagOrder O),(Support (p `^ (t . i))))) /. j) by A21, PARTFUN1:def 6 ;
A24: ((Subst (t,i,p)) * tran) /. j = ((Subst (t,i,p)) * tran) . j by A16, A11, A9, FINSEQ_3:25, A20, PARTFUN1:def 6
.= (Subst (t,i,p)) . (tran . j) by A16, A11, A9, FINSEQ_3:25, A20, FUNCT_1:12
.= ((p `^ (t . i)) * (SgmX ((BagOrder O),(Support (p `^ (t . i)))))) /. j by A23, Th33, A22 ;
( Y . j = Y /. j & Y /. j = (((Subst (t,i,p)) * tran) /. j) * (eval ((tran /. j),x)) ) by A16, A12, A21, PARTFUN1:def 6;
hence Y . j = (((p `^ (t . i)) * (SgmX ((BagOrder O),(Support (p `^ (t . i)))))) /. j) * ((eval ((t +* (i,0)),x)) * (eval (((SgmX ((BagOrder O),(Support (p `^ (t . i))))) /. j),x))) by A22, A24, POLYNOM2:16
.= ((((p `^ (t . i)) * (SgmX ((BagOrder O),(Support (p `^ (t . i)))))) /. j) * (eval (((SgmX ((BagOrder O),(Support (p `^ (t . i))))) /. j),x))) * (eval ((t +* (i,0)),x)) by GROUP_1:def 3
.= (y /. j) * (eval ((t +* (i,0)),x)) by A17, A3, A18, A16
.= (y * (eval ((t +* (i,0)),x))) /. j by A21, POLYNOM1:def 2
.= (y * (eval ((t +* (i,0)),x))) . j by A13, A16, A2, A11, A7, A9, FINSEQ_3:25, PARTFUN1:def 6 ;
:: thesis:

end;

then A25: Y = y * (eval ((t +* (i,0)),x)) by A14, A2, A11, A6, FINSEQ_4:62, A7, FINSEQ_1:14;
dom t = O by PARTFUN1:def 2;
then A26: (t +* (i,0)) . i = 0 by A1, FUNCT_7:31;
( dom x = O & O = dom (x +* (i,(eval (p,x)))) ) by PARTFUN1:def 2;
then A27: ( (x +* (i,(eval (p,x)))) /. i = (x +* (i,(eval (p,x)))) . i & (x +* (i,(eval (p,x)))) . i = eval (p,x) ) by A1, FUNCT_7:31, PARTFUN1:def 6;
( (power R) . (((x +* (i,(eval (p,x)))) /. i),0) = 1_ R & 1_ R = 1. R ) by GROUP_1:def 7;
then (eval ((t +* (i,0)),(x +* (i,(eval (p,x)))))) * ((power R) . (((x +* (i,(eval (p,x)))) /. i),(t . i))) = (eval (t,(x +* (i,(eval (p,x)))))) * (1. R) by A1, Th17;
hence eval (t,(x +* (i,(eval (p,x))))) = ((power R) . ((eval (p,x)),(t . i))) * (eval ((t +* (i,0)),x)) by A26, Th18, A27
.= eval ((Subst (t,i,p)),x) by A25, A15, A2, A11, POLYNOM1:13 ;
:: thesis: