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