let L be non degenerated comRing; for x being Element of L
for n being Element of NAT
for p being Polynomial of L st n < len p holds
eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)
let x be Element of L; for n being Element of NAT
for p being Polynomial of L st n < len p holds
eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)
let n be Element of NAT ; for p being Polynomial of L st n < len p holds
eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)
let p be Polynomial of L; ( n < len p implies eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n) )
assume A1:
n < len p
; eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)
set ps = poly_shift (p,n);
set ps1 = poly_shift (p,(n + 1));
consider f being FinSequence of L such that
A2:
eval ((poly_shift (p,n)),x) = Sum f
and
A3:
len f = len (poly_shift (p,n))
and
A4:
for k being Element of NAT st k in dom f holds
f . k = ((poly_shift (p,n)) . (k -' 1)) * ((power L) . (x,(k -' 1)))
by POLYNOM4:def 2;
consider f1 being FinSequence of L such that
A5:
eval ((poly_shift (p,(n + 1))),x) = Sum f1
and
A6:
len f1 = len (poly_shift (p,(n + 1)))
and
A7:
for k being Element of NAT st k in dom f1 holds
f1 . k = ((poly_shift (p,(n + 1))) . (k -' 1)) * ((power L) . (x,(k -' 1)))
by POLYNOM4:def 2;
( rng f1 c= the carrier of L & dom (x multfield) = the carrier of L )
by FUNCT_2:def 1;
then A8:
( x * f1 = (x multfield) * f1 & dom ((x multfield) * f1) = dom f1 )
by FVSUM_1:def 6, RELAT_1:27;
A9:
1_ L = 1. L
;
now ( len f = len f & len (<*(p . n)*> ^ (x * f1)) = len f & ( for j being Nat st j in dom f holds
f . j = (<*(p . n)*> ^ (x * f1)) . j ) )A10:
n + 1
<= len p
by A1, NAT_1:13;
A11:
((len (poly_shift (p,(n + 1)))) + 1) + n =
(len (poly_shift (p,(n + 1)))) + (n + 1)
.=
len p
by A10, Th41
.=
(len (poly_shift (p,n))) + n
by A1, Th41
;
thus
len f = len f
;
( len (<*(p . n)*> ^ (x * f1)) = len f & ( for j being Nat st j in dom f holds
f . b2 = (<*(p . n)*> ^ (x * f1)) . b2 ) )A12:
len <*(p . n)*> = 1
by FINSEQ_1:40;
A13:
len (x * f1) = len f1
by A8, FINSEQ_3:29;
hence
len (<*(p . n)*> ^ (x * f1)) = len f
by A3, A6, A11, A12, FINSEQ_1:22;
for j being Nat st j in dom f holds
f . b2 = (<*(p . n)*> ^ (x * f1)) . b2let j be
Nat;
( j in dom f implies f . b1 = (<*(p . n)*> ^ (x * f1)) . b1 )assume A14:
j in dom f
;
f . b1 = (<*(p . n)*> ^ (x * f1)) . b1A15:
1
<= j
by A14, FINSEQ_3:25;
A16:
j <= len f
by A14, FINSEQ_3:25;
per cases
( j = 1 or 1 < j )
by A15, XXREAL_0:1;
suppose A17:
j = 1
;
f . b1 = (<*(p . n)*> ^ (x * f1)) . b1A18:
1
in dom <*(p . n)*>
by A12, FINSEQ_3:25;
thus f . j =
((poly_shift (p,n)) . (1 -' 1)) * ((power L) . (x,(1 -' 1)))
by A4, A14, A17
.=
((poly_shift (p,n)) . 0) * ((power L) . (x,(1 -' 1)))
by XREAL_1:232
.=
((poly_shift (p,n)) . 0) * ((power L) . (x,0))
by XREAL_1:232
.=
((poly_shift (p,n)) . 0) * (1. L)
by A9, GROUP_1:def 7
.=
(poly_shift (p,n)) . 0
.=
p . (n + 0)
by Def5
.=
<*(p . n)*> . 1
by FINSEQ_1:40
.=
(<*(p . n)*> ^ (x * f1)) . j
by A17, A18, FINSEQ_1:def 7
;
verum end; suppose A19:
1
< j
;
f . b1 = (<*(p . n)*> ^ (x * f1)) . b1
1
- 1
<= j - 1
by A15, XREAL_1:9;
then reconsider j1 =
j - 1 as
Element of
NAT by INT_1:3;
A20:
1
+ 1
<= j
by A19, NAT_1:13;
then A21:
(1 + 1) - 1
<= j - 1
by XREAL_1:9;
then
ex
j2 being
Nat st
j1 = j2 + 1
by NAT_1:6;
then A22:
(j1 -' 1) + 1
= j1
by NAT_D:34;
j = j1 + 1
;
then A23:
j1 = j -' 1
by NAT_D:34;
j - 1
<= ((len f1) + 1) - 1
by A3, A6, A11, A16, XREAL_1:9;
then A24:
j1 in dom f1
by A21, FINSEQ_3:25;
then reconsider f1j =
f1 . j1 as
Element of
L by FINSEQ_2:11;
thus f . j =
((poly_shift (p,n)) . (j -' 1)) * ((power L) . (x,(j -' 1)))
by A4, A14
.=
(p . (n + j1)) * ((power L) . (x,j1))
by A23, Def5
.=
(p . ((n + 1) + (j1 -' 1))) * (((power L) . (x,(j1 -' 1))) * x)
by A22, GROUP_1:def 7
.=
x * ((p . ((n + 1) + (j1 -' 1))) * ((power L) . (x,(j1 -' 1))))
by GROUP_1:def 3
.=
x * (((poly_shift (p,(n + 1))) . (j1 -' 1)) * ((power L) . (x,(j1 -' 1))))
by Def5
.=
x * f1j
by A7, A24
.=
(x * f1) . j1
by A8, A24, FVSUM_1:50
.=
(<*(p . n)*> ^ (x * f1)) . j
by A3, A6, A11, A12, A13, A16, A20, FINSEQ_1:23
;
verum end;
then
( x * (Sum f1) = Sum (x * f1) & f = <*(p . n)*> ^ (x * f1) )
by FINSEQ_2:9, FVSUM_1:73;
hence
eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)
by A2, A5, FVSUM_1:72; verum