let x be Element of F_Complex; Ext_eval (X^2+X+1,x) = ((x |^ 2) + x) + 1
set R = F_Complex ;
set p = X^2+X+1 ;
set t = 1. F_Complex;
consider F being FinSequence of the carrier of F_Complex such that
A1:
Ext_eval (X^2+X+1,x) = Sum F
and
A2:
len F = len X^2+X+1
and
A3:
for n being Element of NAT st n in dom F holds
F . n = (In ((X^2+X+1 . (n -' 1)),F_Complex)) * ((power F_Complex) . (x,(n -' 1)))
by ALGNUM_1:def 1;
B1: X^2+X+1 . 0 =
1
by GAUSSINT:def 14, FIELD_9:16
.=
1. F_Complex
by COMPLEX1:def 4, COMPLFLD:def 1
;
B2: X^2+X+1 . 1 =
1
by GAUSSINT:def 14, FIELD_9:16
.=
1. F_Complex
by COMPLEX1:def 4, COMPLFLD:def 1
;
B3: X^2+X+1 . 2 =
1
by GAUSSINT:def 14, FIELD_9:16
.=
1. F_Complex
by COMPLEX1:def 4, COMPLFLD:def 1
;
1. F_Rat <> 0. F_Rat
;
then BB:
deg X^2+X+1 = 2
by FIELD_9:18;
B0:
deg X^2+X+1 = (len X^2+X+1) - 1
by HURWITZ:def 2;
then B4:
len F = 3
by A2, BB;
then A5: F . 1 =
(In ((X^2+X+1 . (1 -' 1)),F_Complex)) * ((power F_Complex) . (x,(1 -' 1)))
by A3, FINSEQ_3:25
.=
(In ((X^2+X+1 . 0),F_Complex)) * ((power F_Complex) . (x,(1 -' 1)))
by XREAL_1:232
.=
(X^2+X+1 . 0) * ((power F_Complex) . (x,0))
by XREAL_1:232
.=
(1. F_Complex) * (1_ F_Complex)
by B1, GROUP_1:def 7
;
A6:
2 -' 1 = 2 - 1
by XREAL_0:def 2;
A7: F . 2 =
(In ((X^2+X+1 . (2 -' 1)),F_Complex)) * ((power F_Complex) . (x,(2 -' 1)))
by B4, A3, FINSEQ_3:25
.=
x |^ 1
by B2, A6, BINOM:def 2
.=
x
by BINOM:8
;
A8:
3 -' 1 = 3 - 1
by XREAL_0:def 2;
A9: F . 3 =
(In ((X^2+X+1 . (3 -' 1)),F_Complex)) * ((power F_Complex) . (x,(3 -' 1)))
by B0, A3, A2, BB, FINSEQ_3:25
.=
x |^ 2
by B3, A8, BINOM:def 2
;
F = <*(1. F_Complex),x,(x |^ 2)*>
by B0, A2, BB, A5, A7, A9, FINSEQ_1:45;
hence Ext_eval (X^2+X+1,x) =
((1. F_Complex) + x) + (x |^ 2)
by A1, RLVECT_1:46
.=
((x |^ 2) + x) + 1
by COMPLFLD:8, COMPLEX1:def 4
;
verum