let R be Ring; :: thesis: for a, b, c, x being Element of R holds eval (<%c,b,a%>,x) = (c + (b * x)) + (a * (x ^2))
let a, b, c, x be Element of R; :: thesis: eval (<%c,b,a%>,x) = (c + (b * x)) + (a * (x ^2))
consider F being FinSequence of the carrier of R such that
A1: eval (<%c,b,a%>,x) = Sum F and
A2: len F = len <%c,b,a%> and
A3: for n being Element of NAT st n in dom F holds
F . n = (<%c,b,a%> . (n -' 1)) * ((power R) . (x,(n -' 1))) by POLYNOM4:def 2;
not not len F = 0 & ... & not len F = 3 by A2, qua2;

per cases then ( len F = 0 or len F = 1 or len F = 2 or len F = 3 ) ;

suppose len F = 0 ; :: thesis: eval (<%c,b,a%>,x) = (c + (b * x)) + (a * (x ^2))

then A4: <%c,b,a%> = 0_. R by A2, POLYNOM4:5;
hence eval (<%c,b,a%>,x) = (0_. R) . 0 by POLYNOM4:17
.= c + (((0_. R) . 1) * x) by A4, qua1
.= (c + (b * x)) + (((0_. R) . 2) * (x ^2)) by A4, qua1
.= (c + (b * x)) + (a * (x ^2)) by A4, qua1 ;
:: thesis: verum

end;

suppose A5: len F = 1 ; :: thesis: eval (<%c,b,a%>,x) = (c + (b * x)) + (a * (x ^2))

then 0 + 1 in Seg (len F) by FINSEQ_1:4;
then 1 in dom F by FINSEQ_1:def 3;
then F . 1 = (<%c,b,a%> . (1 -' 1)) * ((power R) . (x,(1 -' 1))) by A3
.= (<%c,b,a%> . 0) * ((power R) . (x,(1 -' 1))) by XREAL_1:232
.= (<%c,b,a%> . 0) * ((power R) . (x,0)) by XREAL_1:232
.= c * ((power R) . (x,0)) by qua1
.= c * (1_ R) by GROUP_1:def 7
.= c ;
then F = <*c*> by A5, FINSEQ_1:40;
hence eval (<%c,b,a%>,x) = c + ((0. R) * x) by A1, RLVECT_1:44
.= c + ((<%c,b,a%> . 1) * x) by A2, A5, ALGSEQ_1:8
.= (c + (b * x)) + ((0. R) * (x ^2)) by qua1
.= (c + (b * x)) + ((<%c,b,a%> . 2) * (x ^2)) by A2, A5, ALGSEQ_1:8
.= (c + (b * x)) + (a * (x ^2)) by qua1 ;
:: thesis: verum

end;

suppose A6: len F = 2 ; :: thesis: eval (<%c,b,a%>,x) = (c + (b * x)) + (a * (x ^2))

then A7: F . 1 = (<%c,b,a%> . (1 -' 1)) * ((power R) . (x,(1 -' 1))) by A3, FINSEQ_3:25
.= (<%c,b,a%> . 0) * ((power R) . (x,(1 -' 1))) by XREAL_1:232
.= (<%c,b,a%> . 0) * ((power R) . (x,0)) by XREAL_1:232
.= c * ((power R) . (x,0)) by qua1
.= c * (1_ R) by GROUP_1:def 7
.= c ;
A8: 2 -' 1 = 2 - 1 by XREAL_0:def 2;
F . 2 = (<%c,b,a%> . (2 -' 1)) * ((power R) . (x,(2 -' 1))) by A3, A6, FINSEQ_3:25
.= b * ((power R) . (x,1)) by A8, qua1
.= b * x by GROUP_1:50 ;
then F = <*c,(b * x)*> by A6, A7, FINSEQ_1:44;
hence eval (<%c,b,a%>,x) = (c + (b * x)) + ((0. R) * (x ^2)) by A1, RLVECT_1:45
.= (c + (b * x)) + ((<%c,b,a%> . 2) * (x ^2)) by A2, A6, ALGSEQ_1:8
.= (c + (b * x)) + (a * (x ^2)) by qua1 ;
:: thesis: verum

end;

suppose A9: len F = 3 ; :: thesis: eval (<%c,b,a%>,x) = (c + (b * x)) + (a * (x ^2))

then A10: F . 1 = (<%c,b,a%> . (1 -' 1)) * ((power R) . (x,(1 -' 1))) by A3, FINSEQ_3:25
.= (<%c,b,a%> . 0) * ((power R) . (x,(1 -' 1))) by XREAL_1:232
.= (<%c,b,a%> . 0) * ((power R) . (x,0)) by XREAL_1:232
.= c * ((power R) . (x,0)) by qua1
.= c * (1_ R) by GROUP_1:def 7
.= c ;
A11: 2 -' 1 = 2 - 1 by XREAL_0:def 2;
A12: F . 2 = (<%c,b,a%> . (2 -' 1)) * ((power R) . (x,(2 -' 1))) by A3, A9, FINSEQ_3:25
.= b * ((power R) . (x,1)) by A11, qua1
.= b * x by GROUP_1:50 ;
A13: 3 -' 1 = 3 - 1 by XREAL_0:def 2;
F . 3 = (<%c,b,a%> . (3 -' 1)) * ((power R) . (x,(3 -' 1))) by A3, A9, FINSEQ_3:25
.= a * ((power R) . (x,2)) by A13, qua1
.= a * (x * x) by GROUP_1:51
.= a * (x ^2) by O_RING_1:def 1 ;
then F = <*c,(b * x),(a * (x ^2))*> by A9, A10, A12, FINSEQ_1:45;
hence eval (<%c,b,a%>,x) = (c + (b * x)) + (a * (x ^2)) by A1, RLVECT_1:46; :: thesis: verum

end;

end;