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)) * (() . (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)) * (() . (x,(k -' 1))) by POLYNOM4:def 2;
( rng f1 c= the carrier of L & dom () = the carrier of L ) by FUNCT_2:def 1;
then A8: ( x * f1 = () * f1 & dom (() * f1) = dom f1 ) by ;
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 ;
A11: ((len (poly_shift (p,(n + 1)))) + 1) + n = (len (poly_shift (p,(n + 1)))) + (n + 1)
.= len p by
.= (len (poly_shift (p,n))) + n by ;
thus len f = len f ; :: thesis: ( 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 ;
hence len (<*(p . n)*> ^ (x * f1)) = len f by ; :: thesis: for j being Nat st j in dom f holds
f . b2 = (<*(p . n)*> ^ (x * f1)) . b2

let j be Nat; :: thesis: ( j in dom f implies f . b1 = (<*(p . n)*> ^ (x * f1)) . b1 )
assume A14: j in dom f ; :: thesis: f . b1 = (<*(p . n)*> ^ (x * f1)) . b1
A15: 1 <= j by ;
A16: j <= len f by ;
per cases ( j = 1 or 1 < j ) by ;
suppose A17: j = 1 ; :: thesis: f . b1 = (<*(p . n)*> ^ (x * f1)) . b1
A18: 1 in dom <*(p . n)*> by ;
thus f . j = ((poly_shift (p,n)) . (1 -' 1)) * (() . (x,(1 -' 1))) by A4, A14, A17
.= ((poly_shift (p,n)) . 0) * (() . (x,(1 -' 1))) by XREAL_1:232
.= ((poly_shift (p,n)) . 0) * (() . (x,0)) by XREAL_1:232
.= ((poly_shift (p,n)) . 0) * (1. L) by
.= (poly_shift (p,n)) . 0
.= p . (n + 0) by Def5
.= <*(p . n)*> . 1 by FINSEQ_1:40
.= (<*(p . n)*> ^ (x * f1)) . j by ; :: thesis: verum
end;
suppose A19: 1 < j ; :: thesis: f . b1 = (<*(p . n)*> ^ (x * f1)) . b1
1 - 1 <= j - 1 by ;
then reconsider j1 = j - 1 as Element of NAT by INT_1:3;
A20: 1 + 1 <= j by ;
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 ;
then A24: j1 in dom f1 by ;
then reconsider f1j = f1 . j1 as Element of L by FINSEQ_2:11;
thus f . j = ((poly_shift (p,n)) . (j -' 1)) * (() . (x,(j -' 1))) by
.= (p . (n + j1)) * (() . (x,j1)) by
.= (p . ((n + 1) + (j1 -' 1))) * ((() . (x,(j1 -' 1))) * x) by
.= x * ((p . ((n + 1) + (j1 -' 1))) * (() . (x,(j1 -' 1)))) by GROUP_1:def 3
.= x * (((poly_shift (p,(n + 1))) . (j1 -' 1)) * (() . (x,(j1 -' 1)))) by Def5
.= x * f1j by
.= (x * f1) . j1 by
.= (<*(p . n)*> ^ (x * f1)) . j by ; :: thesis: verum
end;
end;
end;
then ( x * (Sum f1) = Sum (x * f1) & f = <*(p . n)*> ^ (x * f1) ) by ;
hence eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n) by ; :: thesis: verum