let n be Nat; 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 ; 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; 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; 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; ( y | n = x implies eval (p,x) = eval ((p extended_by_0),y) )
set n1 = n + 1;
assume A1:
y | n = x
; 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;
( 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))) )
;
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
;
verum
end;
hence
eval (p,x) = eval ((p extended_by_0),y)
by FINSEQ_1:14, A2, A4, Th17; verum