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;

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 )
;

end;

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;then a = 0. R by RING_4:19;

hence eval ((a | R),x) = a by POLYNOM4:17, A0; :: thesis: verum

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;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