set F = F_Rat ;
reconsider p1 = X- (1. F_Rat), p2 = X^2+X+1 , q = X^3-1 as Polynomial of F_Rat ;
J: 5 -' 1 = 5 - 1 by XREAL_0:def 2;
L: 4 -' 1 = 4 - 1 by XREAL_0:def 2;
then K: ( 2 -' 1 = 2 - 1 & 3 -' 1 = 3 - 1 & 3 -' 2 = 3 - 2 & 4 -' 1 = 3 & 4 -' 2 = 4 - 2 ) by XREAL_0:def 2;
A: dom (p1 *' p2) = NAT by FUNCT_2:def 1
.= dom q by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom q holds
(p1 *' p2) . o = q . o

let o be object ; :: thesis: ( o in dom q implies (p1 *' p2) . b₁ = q . b₁ )
assume o in dom q ; :: thesis: (p1 *' p2) . b₁ = q . b₁
then reconsider i = o as Element of NAT ;
consider r being FinSequence of the carrier of F_Rat such that
B1: ( len r = i + 1 & (p1 *' p2) . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p1 . (k -' 1)) * (p2 . ((i + 1) -' k)) ) ) by POLYNOM3:def 9;
( i <= 3 implies not not i = 0 & ... & not i = 3 ) ;

per cases then ( i = 0 or i = 1 or i = 2 or i = 3 or i > 3 ) ;

suppose C: i = 0 ; :: thesis: (p1 *' p2) . b₁ = q . b₁

then B2: r = <*(r . 1)*> by B1, FINSEQ_1:40;
then dom r = {1} by FINSEQ_1:2, FINSEQ_1:38;
then 1 in dom r by TARSKI:def 1;
then r . 1 = (p1 . (1 -' 1)) * (p2 . ((0 + 1) -' 1)) by C, B1
.= (p1 . (1 -' 1)) * (p2 . 0) by NAT_2:8
.= (p1 . 0) * (p2 . 0) by NAT_2:8
.= ((rpoly (1,(1. F_Rat))) . 0) * (p2 . 0) by FIELD_9:def 2
.= (- ((power F_Rat) . ((1. F_Rat),1))) * (p2 . 0) by HURWITZ:25
.= (- ((1. F_Rat) |^ 1)) * (p2 . 0) by BINOM:def 2
.= (- (1. F_Rat)) * (p2 . 0) by BINOM:8
.= (- (1. F_Rat)) * (1. F_Rat) by FIELD_9:16 ;
hence (p1 *' p2) . o = q . o by B1, C, LL01, GAUSSINT:13, B2, RLVECT_1:44; :: thesis: verum

end;

suppose C: i = 1 ; :: thesis: (p1 *' p2) . b₁ = q . b₁

then B3: r = <*(r . 1),(r . 2)*> by B1, FINSEQ_1:44;
B4: dom r = {1,2} by B1, C, FINSEQ_1:def 3, FINSEQ_1:2;
then 1 in dom r by TARSKI:def 2;
then B5: r . 1 = (p1 . (1 -' 1)) * (p2 . ((1 + 1) -' 1)) by C, B1
.= (p1 . 0) * (p2 . 1) by K, NAT_2:8
.= ((rpoly (1,(1. F_Rat))) . 0) * (p2 . 1) by FIELD_9:def 2
.= (- ((power F_Rat) . ((1. F_Rat),1))) * (p2 . 1) by HURWITZ:25
.= (- ((1. F_Rat) |^ 1)) * (p2 . 1) by BINOM:def 2
.= (- (1. F_Rat)) * (p2 . 1) by BINOM:8
.= (- (1. F_Rat)) * (1. F_Rat) by FIELD_9:16 ;
2 in dom r by B4, TARSKI:def 2;
then r . 2 = (p1 . (2 -' 1)) * (p2 . ((1 + 1) -' 2)) by C, B1
.= (p1 . 1) * (p2 . 0) by K, NAT_2:8
.= ((rpoly (1,(1. F_Rat))) . 1) * (p2 . 0) by FIELD_9:def 2
.= (1_ F_Rat) * (p2 . 0) by HURWITZ:25
.= 1. F_Rat by FIELD_9:16 ;
then Sum r = (- (1. F_Rat)) + (1. F_Rat) by B3, B5, RLVECT_1:45
.= 0 ;
hence (p1 *' p2) . o = q . o by B1, C, LL01; :: thesis: verum

end;

suppose C: i = 2 ; :: thesis: (p1 *' p2) . b₁ = q . b₁

then B3: r = <*(r . 1),(r . 2),(r . 3)*> by B1, FINSEQ_1:45;
B4: dom r = Seg 3 by B1, C, FINSEQ_1:def 3
.= (Seg 2) \/ {(2 + 1)} by FINSEQ_1:9
.= {1,2,3} by FINSEQ_1:2, ENUMSET1:3 ;
then 1 in dom r by ENUMSET1:def 1;
then B5: r . 1 = (p1 . (1 -' 1)) * (p2 . ((2 + 1) -' 1)) by C, B1
.= (p1 . 0) * (p2 . 2) by K, NAT_2:8
.= (p1 . 0) * (1. F_Rat) by FIELD_9:16
.= (rpoly (1,(1. F_Rat))) . 0 by FIELD_9:def 2
.= - ((power F_Rat) . ((1. F_Rat),1)) by HURWITZ:25
.= - ((1. F_Rat) |^ 1) by BINOM:def 2
.= - (1. F_Rat) by BINOM:8 ;
2 in dom r by B4, ENUMSET1:def 1;
then B6: r . 2 = (p1 . 1) * (p2 . 1) by K, C, B1
.= (p1 . 1) * (1. F_Rat) by FIELD_9:16
.= (rpoly (1,(1. F_Rat))) . 1 by FIELD_9:def 2
.= 1_ F_Rat by HURWITZ:25
.= 1. F_Rat ;
3 in dom r by B4, ENUMSET1:def 1;
then r . 3 = (p1 . 2) * (p2 . ((2 + 1) -' 3)) by K, C, B1
.= ((rpoly (1,(1. F_Rat))) . 2) * (p2 . ((2 + 1) -' 3)) by FIELD_9:def 2
.= (0. F_Rat) * (p2 . ((2 + 1) -' 3)) by HURWITZ:26 ;
then Sum r = ((- (1. F_Rat)) + (1. F_Rat)) + (0. F_Rat) by B3, B5, B6, RLVECT_1:46
.= 0 ;
hence (p1 *' p2) . o = q . o by B1, C, LL01; :: thesis: verum

end;

suppose C: i = 3 ; :: thesis: (p1 *' p2) . b₁ = q . b₁

then B3: r = <*(r . 1),(r . 2),(r . 3),(r . 4)*> by B1, FINSEQ_4:76;
B4: dom r = Seg 4 by B1, C, FINSEQ_1:def 3
.= (Seg 3) \/ {(3 + 1)} by FINSEQ_1:9
.= ((Seg 2) \/ {(2 + 1)}) \/ {4} by FINSEQ_1:9
.= {1,2,3} \/ {4} by FINSEQ_1:2, ENUMSET1:3
.= {1,2,3,4} by ENUMSET1:6 ;
then 1 in dom r by ENUMSET1:def 2;
then B5: r . 1 = (p1 . (1 -' 1)) * (p2 . ((3 + 1) -' 1)) by C, B1
.= (p1 . 0) * (p2 . 3) by L, NAT_2:8
.= (p1 . 0) * (0. F_Rat) by FIELD_9:16 ;
2 in dom r by B4, ENUMSET1:def 2;
then B6: r . 2 = (p1 . 1) * (p2 . 2) by K, C, B1
.= (p1 . 1) * (1. F_Rat) by FIELD_9:16
.= (rpoly (1,(1. F_Rat))) . 1 by FIELD_9:def 2
.= 1_ F_Rat by HURWITZ:25
.= 1. F_Rat ;
3 in dom r by B4, ENUMSET1:def 2;
then B7: r . 3 = (p1 . 2) * (p2 . ((3 + 1) -' 3)) by K, C, B1
.= ((rpoly (1,(1. F_Rat))) . 2) * (p2 . ((3 + 1) -' 3)) by FIELD_9:def 2
.= (0. F_Rat) * (p2 . ((3 + 1) -' 3)) by HURWITZ:26 ;
4 in dom r by B4, ENUMSET1:def 2;
then r . 4 = (p1 . 3) * (p2 . ((3 + 1) -' 4)) by L, C, B1
.= ((rpoly (1,(1. F_Rat))) . 3) * (p2 . ((3 + 1) -' 4)) by FIELD_9:def 2
.= (0. F_Rat) * (p2 . ((3 + 1) -' 4)) by HURWITZ:26 ;
then r = <*(0. F_Rat),(1. F_Rat),(0. F_Rat)*> ^ <*(0. F_Rat)*> by B3, B5, B6, B7, FINSEQ_4:74;
then Sum r = (Sum <*(0. F_Rat),(1. F_Rat),(0. F_Rat)*>) + (Sum <*(0. F_Rat)*>) by RLVECT_1:41
.= (Sum <*(0. F_Rat),(1. F_Rat),(0. F_Rat)*>) + (0. F_Rat) by RLVECT_1:44
.= 1 by RLVECT_1:72, GAUSSINT:13 ;
hence (p1 *' p2) . o = q . o by B1, C, LL01; :: thesis: verum

end;

suppose C: i > 3 ; :: thesis: (p1 *' p2) . b₁ = q . b₁

C0: deg q = (len q) - 1 by HURWITZ:def 2;
C1: i >= 3 + 1 by C, NAT_1:13;
then E: q . i = 0. F_Rat by C0, LL, ALGSEQ_1:8;
p1 = rpoly (1,(1. F_Rat)) by FIELD_9:def 2;
then C2: ( deg p1 = 1 & deg p2 = 2 ) by LL, HURWITZ:27;
F: ( deg p1 = (len p1) - 1 & deg p2 = (len p2) - 1 ) by HURWITZ:def 2;
len (p1 *' p2) <= ((len p1) + (len p2)) -' 1 by leng;
hence (p1 *' p2) . o = q . o by J, F, C2, C1, XXREAL_0:2, E, ALGSEQ_1:8; :: thesis: verum

end;

end;

end;

then q = p1 *' p2 by A
.= (X- (1. F_Rat)) * X^2+X+1 by POLYNOM3:def 10 ;
hence X^3-1 = (X- (1. F_Rat)) * X^2+X+1 ; :: thesis: verum