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:27;
A9: 1_ L = 1. L ;

now :: thesis: ( 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 ; :: 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: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; :: 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: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 ; :: thesis: f . b₁ = (<*(p . n)*> ^ (x * f1)) . b₁

A18: 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
.= (<*(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: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 ; :: thesis: verum

end;

end;

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; :: thesis: verum