let O be Ordinal; :: thesis: for R being non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p, s being Polynomial of O,R
for i being object
for x being Function of O,R st i in O holds
eval ((Subst (p,i,s)),x) = eval (p,(x +* (i,(eval (s,x)))))
let R be non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p, s being Polynomial of O,R
for i being object
for x being Function of O,R st i in O holds
eval ((Subst (p,i,s)),x) = eval (p,(x +* (i,(eval (s,x)))))
let p, s be Polynomial of O,R; :: thesis: for i being object
for x being Function of O,R st i in O holds
eval ((Subst (p,i,s)),x) = eval (p,(x +* (i,(eval (s,x)))))
let i be object ; :: thesis: for x being Function of O,R st i in O holds
eval ((Subst (p,i,s)),x) = eval (p,(x +* (i,(eval (s,x)))))
let x be Function of O,R; :: thesis: ( i in O implies eval ((Subst (p,i,s)),x) = eval (p,(x +* (i,(eval (s,x))))) )
assume A1: i in O ; :: thesis: eval ((Subst (p,i,s)),x) = eval (p,(x +* (i,(eval (s,x)))))
set Sub = Subst (p,i,s);
set xE = x +* (i,(eval (s,x)));
set B = SgmX ((BagOrder O),(Support p));
consider f being FinSequence of R such that
A2: ( len f = len (SgmX ((BagOrder O),(Support p))) & eval (p,(x +* (i,(eval (s,x))))) = Sum f ) and
A3: for j being Element of NAT st 1 <= j & j <= len f holds
f /. j = ((p * (SgmX ((BagOrder O),(Support p)))) /. j) * (eval (((SgmX ((BagOrder O),(Support p))) /. j),(x +* (i,(eval (s,x)))))) by POLYNOM2:def 4;
consider S being FinSequence of (Polynom-Ring (O,R)) such that
A4: ( Subst (p,i,s) = Sum S & len (SgmX ((BagOrder O),(Support p))) = len S ) and
A5: for j being Nat st j in dom S holds
S . j = (p . ((SgmX ((BagOrder O),(Support p))) /. j)) * (Subst (((SgmX ((BagOrder O),(Support p))) /. j),i,s)) by Def4;
for q being Polynomial of O,R
for j being Nat st j in dom f & q = S . j holds
f . j = eval (q,x)

proof

let q be Polynomial of O,R; :: thesis: for j being Nat st j in dom f & q = S . j holds
f . j = eval (q,x)
let j be Nat; :: thesis: ( j in dom f & q = S . j implies f . j = eval (q,x) )
assume A6: ( j in dom f & q = S . j ) ; :: thesis: f . j = eval (q,x)
A7: ( dom f = dom S & dom S = dom (SgmX ((BagOrder O),(Support p))) ) by A2, A4, FINSEQ_3:29;
then S . j = (p . ((SgmX ((BagOrder O),(Support p))) /. j)) * (Subst (((SgmX ((BagOrder O),(Support p))) /. j),i,s)) by A6, A5;
then A8: eval (q,x) = (p . ((SgmX ((BagOrder O),(Support p))) /. j)) * (eval ((Subst (((SgmX ((BagOrder O),(Support p))) /. j),i,s)),x)) by A6, POLYNOM7:29
.= (p . ((SgmX ((BagOrder O),(Support p))) /. j)) * (eval (((SgmX ((BagOrder O),(Support p))) /. j),(x +* (i,(eval (s,x)))))) by Th35, A1 ;
BagOrder O linearly_orders Support p by POLYNOM2:18;
then A9: rng (SgmX ((BagOrder O),(Support p))) = Support p by PRE_POLY:def 2;
dom p = Bags O by FUNCT_2:def 1;
then dom (p * (SgmX ((BagOrder O),(Support p)))) = dom (SgmX ((BagOrder O),(Support p))) by A9, RELAT_1:27;
then A10: ( (p * (SgmX ((BagOrder O),(Support p)))) /. j = (p * (SgmX ((BagOrder O),(Support p)))) . j & (p * (SgmX ((BagOrder O),(Support p)))) . j = p . ((SgmX ((BagOrder O),(Support p))) . j) & (SgmX ((BagOrder O),(Support p))) /. j = (SgmX ((BagOrder O),(Support p))) . j ) by A6, A7, PARTFUN1:def 6, FUNCT_1:13;
( 1 <= j & j <= len f & j in NAT ) by A6, FINSEQ_3:25;
then ( f . j = f /. j & f /. j = ((p * (SgmX ((BagOrder O),(Support p)))) /. j) * (eval (((SgmX ((BagOrder O),(Support p))) /. j),(x +* (i,(eval (s,x)))))) ) by A3, A6, PARTFUN1:def 6;
hence f . j = eval (q,x) by A8, A10; :: thesis: verum

end;

hence eval ((Subst (p,i,s)),x) = eval (p,(x +* (i,(eval (s,x))))) by A4, Th36, A2; :: thesis: verum