let R be Ring; :: thesis: for a, b being Element of R holds eval ((a | R),b) = a
let a, x be Element of R; :: thesis: eval ((a | R),x) = a
set q = a | R;
consider F being FinSequence of R such that
A3: eval ((a | R),x) = Sum F and
A4: len F = len (a | R) and
A5: for j being Element of NAT st j in dom F holds
F . j = ((a | R) . (j -' 1)) * ((power R) . (x,(j -' 1))) by POLYNOM4:def 2;

per cases ( a | R = 0_. R or a | R <> 0_. R ) ;

suppose A0: a | R = 0_. R ; :: thesis: eval ((a | R),x) = a

then a | R = (0. R) | R by RING_4:13;
then a = 0. R by RING_4:19;
hence eval ((a | R),x) = a by POLYNOM4:17, A0; :: thesis: verum

end;

suppose a | R <> 0_. R ; :: thesis: eval ((a | R),x) = a

then a | R <> (0. R) | R by RING_4:13;
then B: 0 = deg (a | R) by RING_4:21
.= (len (a | R)) - 1 by HURWITZ:def 2 ;
then 1 in Seg (len F) by A4, FINSEQ_1:1;
then 1 in dom F by FINSEQ_1:def 3;
then F . 1 = ((a | R) . (1 -' 1)) * ((power R) . (x,(1 -' 1))) by A5;
then F = <*(((a | R) . (1 -' 1)) * ((power R) . (x,(1 -' 1))))*> by A4, B, FINSEQ_1:40
.= <*(((a | R) . 0) * ((power R) . (x,(1 -' 1))))*> by XREAL_1:232
.= <*(((a | R) . 0) * ((power R) . (x,0)))*> by XREAL_1:232
.= <*(a * ((power R) . (x,0)))*> by Th28
.= <*(a * (1_ R))*> by GROUP_1:def 7
.= <*a*> ;
hence eval ((a | R),x) = a by A3, RLVECT_1:44; :: thesis: verum

end;

end;