let X be Ordinal; :: thesis: for S being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of X,S
for i being object
for x being Function of X,S st i in X \ (vars p) holds
for s being Element of S holds eval (p,x) = eval (p,(x +* (i,s)))
let S be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of X,S
for i being object
for x being Function of X,S st i in X \ (vars p) holds
for s being Element of S holds eval (p,x) = eval (p,(x +* (i,s)))
let p be Polynomial of X,S; :: thesis: for i being object
for x being Function of X,S st i in X \ (vars p) holds
for s being Element of S holds eval (p,x) = eval (p,(x +* (i,s)))
let o be object ; :: thesis: for x being Function of X,S st o in X \ (vars p) holds
for s being Element of S holds eval (p,x) = eval (p,(x +* (o,s)))
let x be Function of X,S; :: thesis: ( o in X \ (vars p) implies for s being Element of S holds eval (p,x) = eval (p,(x +* (o,s))) )
assume A1: o in X \ (vars p) ; :: thesis: for s being Element of S holds eval (p,x) = eval (p,(x +* (o,s)))
let s be Element of S; :: thesis: eval (p,x) = eval (p,(x +* (o,s)))
set xo = x +* (o,s);
set SB = SgmX ((BagOrder X),(Support p));
consider y being FinSequence of the carrier of S such that
A2: ( len y = len (SgmX ((BagOrder X),(Support p))) & eval (p,x) = Sum y ) and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((BagOrder X),(Support p)))) /. i) * (eval (((SgmX ((BagOrder X),(Support p))) /. i),x)) by POLYNOM2:def 4;
consider yo being FinSequence of the carrier of S such that
A4: ( len yo = len (SgmX ((BagOrder X),(Support p))) & eval (p,(x +* (o,s))) = Sum yo ) and
A5: for i being Element of NAT st 1 <= i & i <= len yo holds
yo /. i = ((p * (SgmX ((BagOrder X),(Support p)))) /. i) * (eval (((SgmX ((BagOrder X),(Support p))) /. i),(x +* (o,s)))) by POLYNOM2:def 4;
for i being Nat st 1 <= i & i <= len (SgmX ((BagOrder X),(Support p))) holds
y . i = yo . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (SgmX ((BagOrder X),(Support p))) implies y . i = yo . i )
assume A6: ( 1 <= i & i <= len (SgmX ((BagOrder X),(Support p))) ) ; :: thesis: y . i = yo . i
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A7: ( i in dom (SgmX ((BagOrder X),(Support p))) & i in dom y & i in dom yo ) by A6, A2, A4, FINSEQ_3:25;
then A8: ( (SgmX ((BagOrder X),(Support p))) /. i = (SgmX ((BagOrder X),(Support p))) . i & (SgmX ((BagOrder X),(Support p))) . i in rng (SgmX ((BagOrder X),(Support p))) ) by PARTFUN1:def 6, FUNCT_1:def 3;
BagOrder X linearly_orders Support p by POLYNOM2:18;
then A9: (SgmX ((BagOrder X),(Support p))) /. i in Support p by A8, PRE_POLY:def 2;
not o in vars p by A1, XBOOLE_0:def 5;
then ((SgmX ((BagOrder X),(Support p))) /. i) . o = 0 by A9, Def5;
then eval (((SgmX ((BagOrder X),(Support p))) /. i),x) = eval (((SgmX ((BagOrder X),(Support p))) /. i),(x +* (o,s))) by Th18;
then yo /. i = ((p * (SgmX ((BagOrder X),(Support p)))) /. i) * (eval (((SgmX ((BagOrder X),(Support p))) /. i),x)) by A4, A5, A6;
then ( yo /. i = y /. i & y /. i = y . i ) by A2, A3, A6, A7, PARTFUN1:def 6;
hence y . i = yo . i by A7, PARTFUN1:def 6; :: thesis: verum

end;

hence eval (p,x) = eval (p,(x +* (o,s))) by A4, A2, FINSEQ_1:14; :: thesis: verum