let R be Ring; 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; 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 A5:
len F = 1
;
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
;
verum end; suppose A6:
len F = 2
;
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
;
verum end; suppose A9:
len F = 3
;
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;
verum end; end;