set R = F_Real ;
set p = X^3-2 ;
set x = 3-Root(2) ;
set t = - ((1. F_Real) + (1. F_Real));
consider F being FinSequence of the carrier of F_Real such that
A1:
Ext_eval (X^3-2,3-Root(2)) = Sum F
and
A2:
len F = len X^3-2
and
A3:
for n being Element of NAT st n in dom F holds
F . n = (In ((X^3-2 . (n -' 1)),F_Real)) * ((power F_Real) . (3-Root(2),(n -' 1)))
by ALGNUM_1:def 1;
A5: F . 1 =
(In ((X^3-2 . (1 -' 1)),F_Real)) * ((power F_Real) . (3-Root(2),(1 -' 1)))
by A3, A2, LL1, FINSEQ_3:25
.=
(In ((X^3-2 . 0),F_Real)) * ((power F_Real) . (3-Root(2),(1 -' 1)))
by XREAL_1:232
.=
(X^3-2 . 0) * ((power F_Real) . (3-Root(2),0))
by XREAL_1:232
.=
(- ((1. F_Real) + (1. F_Real))) * (1_ F_Real)
by GROUP_1:def 7, LL0
;
A6:
2 -' 1 = 2 - 1
by XREAL_0:def 2;
A7: F . 2 =
(In ((X^3-2 . (2 -' 1)),F_Real)) * ((power F_Real) . (3-Root(2),(2 -' 1)))
by A3, A2, LL1, FINSEQ_3:25
.=
(0. F_Real) * ((power F_Real) . (3-Root(2),1))
by A6, LL0
;
A8:
3 -' 1 = 3 - 1
by XREAL_0:def 2;
A9: F . 3 =
(In ((X^3-2 . (3 -' 1)),F_Real)) * ((power F_Real) . (3-Root(2),(3 -' 1)))
by A3, A2, LL1, FINSEQ_3:25
.=
(0. F_Real) * ((power F_Real) . (3-Root(2),2))
by A8, LL0
;
A10:
4 -' 1 = 4 - 1
by XREAL_0:def 2;
A11: F . 4 =
(In ((X^3-2 . (4 -' 1)),F_Real)) * ((power F_Real) . (3-Root(2),(4 -' 1)))
by A3, A2, LL1, FINSEQ_3:25
.=
3-Root(2) |^ 3
by A10, LL0, BINOM:def 2
;
F =
<*(- ((1. F_Real) + (1. F_Real))),(0. F_Real),(0. F_Real),(3-Root(2) |^ 3)*>
by A2, LL1, A5, A7, A9, A11, FINSEQ_4:76
.=
<*(- ((1. F_Real) + (1. F_Real))),(0. F_Real),(0. F_Real)*> ^ <*(3-Root(2) |^ 3)*>
by FINSEQ_4:74
;
hence Ext_eval (X^3-2,3-Root(2)) =
(Sum <*(- ((1. F_Real) + (1. F_Real))),(0. F_Real),(0. F_Real)*>) + (Sum <*(3-Root(2) |^ 3)*>)
by A1, RLVECT_1:41
.=
(Sum <*(- ((1. F_Real) + (1. F_Real))),(0. F_Real),(0. F_Real)*>) + (3-Root(2) |^ 3)
by RLVECT_1:44
.=
(3-Root(2) |^ 3) + (- ((1. F_Real) + (1. F_Real)))
by RLVECT_1:72
.=
0. F_Real
by R32
;
verum