let L be non degenerated comRing; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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:46;
A9: 1_ L = 1. L ;

now

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, Th46
.= (len (poly_shift p,n)) + n by A1, Th46 ;
thus len f = len f ; :: thesis: ( len (<*(p . n)*> ^ (x * f1)) = len f & ( for j being Nat st j in dom f holds
f . b₂ = (<*(p . n)*> ^ (x * f1)) . b₂ ) )
A12: len <*(p . n)*> = 1 by FINSEQ_1:57;
A13: len (x * f1) = len f1 by A8, FINSEQ_3:31;
hence len (<*(p . n)*> ^ (x * f1)) = len f by A3, A6, A11, A12, FINSEQ_1:35; :: thesis: for j being Nat st j in dom f holds
f . b₂ = (<*(p . n)*> ^ (x * f1)) . b₂
let j be Nat; :: thesis: ( j in dom f implies f . b₁ = (<*(p . n)*> ^ (x * f1)) . b₁ )
assume A14: j in dom f ; :: thesis: f . b₁ = (<*(p . n)*> ^ (x * f1)) . b₁
A15: 1 <= j by A14, FINSEQ_3:27;
A16: j <= len f by A14, FINSEQ_3:27;

per cases ( j = 1 or 1 < j ) by A15, XXREAL_0:1;

suppose A17: j = 1 ; :: thesis: f . b₁ = (<*(p . n)*> ^ (x * f1)) . b₁

A18: 1 in dom <*(p . n)*> by A12, FINSEQ_3:27;
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:234
.= ((poly_shift p,n) . 0 ) * ((power L) . x,0 ) by XREAL_1:234
.= ((poly_shift p,n) . 0 ) * (1. L) by A9, GROUP_1:def 8
.= (poly_shift p,n) . 0 by A9, GROUP_1:def 5
.= p . (n + 0 ) by Def6
.= <*(p . n)*> . 1 by FINSEQ_1:57
.= (<*(p . n)*> ^ (x * f1)) . j by A17, A18, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A19: 1 < j ; :: thesis: f . b₁ = (<*(p . n)*> ^ (x * f1)) . b₁

1 - 1 <= j - 1 by A15, XREAL_1:11;
then reconsider j1 = j - 1 as Element of NAT by INT_1:16;
A20: 1 + 1 <= j by A19, NAT_1:13;
then A21: (1 + 1) - 1 <= j - 1 by XREAL_1:11;
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:11;
then A24: j1 in dom f1 by A21, FINSEQ_3:27;
then reconsider f1j = f1 . j1 as Element of L by FINSEQ_2:13;
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, Def6
.= (p . ((n + 1) + (j1 -' 1))) * (((power L) . x,(j1 -' 1)) * x) by A22, GROUP_1:def 8
.= x * ((p . ((n + 1) + (j1 -' 1))) * ((power L) . x,(j1 -' 1))) by GROUP_1:def 4
.= x * (((poly_shift p,(n + 1)) . (j1 -' 1)) * ((power L) . x,(j1 -' 1))) by Def6
.= x * f1j by A7, A24
.= (x * f1) . j1 by A8, A24, FVSUM_1:62
.= (<*(p . n)*> ^ (x * f1)) . j by A3, A6, A11, A12, A13, A16, A20, FINSEQ_1:36 ; :: thesis: verum

end;

end;

end;

then ( x * (Sum f1) = Sum (x * f1) & f = <*(p . n)*> ^ (x * f1) ) by FINSEQ_2:10, FVSUM_1:92;
hence eval (poly_shift p,n),x = (x * (eval (poly_shift p,(n + 1)),x)) + (p . n) by A2, A5, FVSUM_1:89; :: thesis: verum