let n be Nat; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L
for x being Function of n,L
for y being Function of (n + 1),L st y | n = x holds
eval (p,x) = eval ((p extended_by_0),y)
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of n,L
for x being Function of n,L
for y being Function of (n + 1),L st y | n = x holds
eval (p,x) = eval ((p extended_by_0),y)
let p be Polynomial of n,L; :: thesis: for x being Function of n,L
for y being Function of (n + 1),L st y | n = x holds
eval (p,x) = eval ((p extended_by_0),y)
let x be Function of n,L; :: thesis: for y being Function of (n + 1),L st y | n = x holds
eval (p,x) = eval ((p extended_by_0),y)
let y be Function of (n + 1),L; :: thesis: ( y | n = x implies eval (p,x) = eval ((p extended_by_0),y) )
set n1 = n + 1;
assume A1: y | n = x ; :: thesis: eval (p,x) = eval ((p extended_by_0),y)
set S = SgmX ((BagOrder n),(Support p));
set P = p extended_by_0 ;
set S1 = SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)));
consider T being FinSequence of L such that
A2: ( len T = len (SgmX ((BagOrder n),(Support p))) & eval (p,x) = Sum T ) and
A3: for i being Element of NAT st 1 <= i & i <= len T holds
T /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) by POLYNOM2:def 4;
consider T1 being FinSequence of L such that
A4: ( len T1 = len (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) & eval ((p extended_by_0),y) = Sum T1 ) and
A5: for i being Element of NAT st 1 <= i & i <= len T1 holds
T1 /. i = (((p extended_by_0) * (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0))))) /. i) * (eval (((SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i),y)) by POLYNOM2:def 4;
A6: ( len (SgmX ((BagOrder n),(Support p))) = len (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) & ( for i being Nat st 1 <= i & i <= len (SgmX ((BagOrder n),(Support p))) holds
(SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i = ((SgmX ((BagOrder n),(Support p))) /. i) bag_extend 0 ) ) by Th17;
( BagOrder n linearly_orders Support p & BagOrder (n + 1) linearly_orders Support (p extended_by_0) ) by POLYNOM2:18;
then A7: ( rng (SgmX ((BagOrder n),(Support p))) = Support p & rng (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) = Support (p extended_by_0) ) by PRE_POLY:def 2;
( dom p = Bags n & dom (p extended_by_0) = Bags (n + 1) ) by FUNCT_2:def 1;
then A8: ( dom (p * (SgmX ((BagOrder n),(Support p)))) = dom (SgmX ((BagOrder n),(Support p))) & dom ((p extended_by_0) * (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0))))) = dom (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) ) by A7, RELAT_1:27;
for i being Nat st 1 <= i & i <= len (SgmX ((BagOrder n),(Support p))) holds
T . i = T1 . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (SgmX ((BagOrder n),(Support p))) implies T . i = T1 . i )
assume A9: ( 1 <= i & i <= len (SgmX ((BagOrder n),(Support p))) ) ; :: thesis: T . i = T1 . i
A10: i in NAT by ORDINAL1:def 12;
A11: ( i in dom T & i in dom T1 ) by A9, A6, A2, A4, FINSEQ_3:25;
A12: ( i in dom (SgmX ((BagOrder n),(Support p))) & i in dom (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) ) by A9, A6, FINSEQ_3:25;
then A13: ( (SgmX ((BagOrder n),(Support p))) /. i = (SgmX ((BagOrder n),(Support p))) . i & (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i = (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) . i ) by PARTFUN1:def 6;
A14: (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i = ((SgmX ((BagOrder n),(Support p))) /. i) bag_extend 0 by Th17, A9;
A15: ((p extended_by_0) * (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0))))) /. i = ((p extended_by_0) * (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0))))) . i by A9, A6, FINSEQ_3:25, A8, PARTFUN1:def 6
.= (p extended_by_0) . ((SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i) by A12, A13, FUNCT_1:13
.= (p extended_by_0) . (((SgmX ((BagOrder n),(Support p))) /. i) bag_extend 0) by Th17, A9
.= p . ((SgmX ((BagOrder n),(Support p))) /. i) by Th6
.= p . ((SgmX ((BagOrder n),(Support p))) . i) by A12, PARTFUN1:def 6
.= (p * (SgmX ((BagOrder n),(Support p)))) . i by A12, FUNCT_1:13
.= (p * (SgmX ((BagOrder n),(Support p)))) /. i by A9, FINSEQ_3:25, A8, PARTFUN1:def 6 ;
thus T1 . i = T1 /. i by A11, PARTFUN1:def 6
.= (((p extended_by_0) * (SgmX ((BagOrder (n + 1)),(Support (p extended_by_0))))) /. i) * (eval (((SgmX ((BagOrder (n + 1)),(Support (p extended_by_0)))) /. i),y)) by A10, A5, A9, A4, A6
.= ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) by A14, Th13, A1, A15
.= T /. i by A10, A3, A9, A2
.= T . i by A11, PARTFUN1:def 6 ; :: thesis: verum

end;

hence eval (p,x) = eval ((p extended_by_0),y) by FINSEQ_1:14, A2, A4, Th17; :: thesis: verum