set F = F_Complex ;
the carrier of (Polynom-Ring F_Rat) c= the carrier of (Polynom-Ring F_Complex) by FIELD_4:10;
then X^2+X+1 is Element of the carrier of (Polynom-Ring F_Complex) ;
then reconsider q = X^2+X+1 as Polynomial of F_Complex ;
reconsider p1 = X- zeta, p2 = X- (zeta ^2) as Polynomial of F_Complex ;
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 ;
B: zeta |^ 2 = zeta ^2 by lemI;
D0: ( q . 0 = 1. F_Rat & q . 1 = 1. F_Rat & q . 2 = 1. F_Rat ) by FIELD_9:16;
1 = 1. F_Complex by COMPLFLD:def 1, COMPLEX1:def 4;
then (- zeta) - 1 = (- zeta) - (1. F_Complex) by COMPLFLD:3;
then D2: - ((- zeta) - 1) = - ((- zeta) - (1. F_Complex)) by COMPLFLD:2
.= (1. F_Complex) + (- (- zeta)) by RLVECT_1:33
.= zeta + (1. F_Complex) ;

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_Complex 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 <= 2 implies not not i = 0 & ... & not i = 2 ) ;

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

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,zeta)) . 0) * (p2 . 0) by FIELD_9:def 2
.= (- ((power F_Complex) . (zeta,1))) * (p2 . 0) by HURWITZ:25
.= (- (zeta |^ 1)) * (p2 . 0) by BINOM:def 2
.= (- zeta) * (p2 . 0) by BINOM:8
.= (- zeta) * ((rpoly (1,(zeta ^2))) . 0) by FIELD_9:def 2
.= (- zeta) * (- ((power F_Complex) . ((zeta ^2),1))) by HURWITZ:25
.= (- zeta) * (- ((zeta ^2) |^ 1)) by BINOM:def 2
.= (- zeta) * (- (zeta |^ 2)) by B, BINOM:8
.= zeta * (zeta |^ 2) by VECTSP_1:10
.= (zeta |^ 2) * (zeta |^ 1) by BINOM:8
.= zeta |^ (2 + 1) by BINOM:10
.= 1. F_Complex by LZ23, COMPLEX1:def 4, COMPLFLD:def 1 ;
hence (p1 *' p2) . o = 1. F_Complex by B1, B2, RLVECT_1:44
.= q . o by C, D0, GAUSSINT:13, COMPLEX1:def 4, COMPLFLD:def 1 ;
:: 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,zeta)) . 0) * (p2 . 1) by FIELD_9:def 2
.= (- ((power F_Complex) . (zeta,1))) * (p2 . 1) by HURWITZ:25
.= (- (zeta |^ 1)) * (p2 . 1) by BINOM:def 2
.= (- zeta) * (p2 . 1) by BINOM:8
.= (- zeta) * ((rpoly (1,(zeta ^2))) . 1) by FIELD_9:def 2
.= (- zeta) * (1_ F_Complex) by HURWITZ:25
.= - zeta ;
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,zeta)) . 1) * (p2 . 0) by FIELD_9:def 2
.= (1_ F_Complex) * (p2 . 0) by HURWITZ:25
.= (rpoly (1,(zeta ^2))) . 0 by FIELD_9:def 2
.= - ((power F_Complex) . ((zeta ^2),1)) by HURWITZ:25
.= - ((zeta ^2) |^ 1) by BINOM:def 2
.= zeta + (1. F_Complex) by D2, B, LZ23, COMPLFLD:2, BINOM:8 ;
then Sum r = (- zeta) + (zeta + (1. F_Complex)) by B3, B5, RLVECT_1:45
.= ((- zeta) + zeta) + (1. F_Complex)
.= (0. F_Complex) + (1. F_Complex) by RLVECT_1:5 ;
hence (p1 *' p2) . o = q . o by C, D0, B1, COMPLFLD:def 1, GAUSSINT:13, COMPLEX1:def 4; :: 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) * ((rpoly (1,(zeta ^2))) . 2) by FIELD_9:def 2
.= (p1 . 0) * (0. F_Complex) by HURWITZ:26 ;
2 in dom r by B4, ENUMSET1:def 1;
then B6: r . 2 = (p1 . 1) * (p2 . 1) by K, C, B1
.= ((rpoly (1,zeta)) . 1) * (p2 . 1) by FIELD_9:def 2
.= (1_ F_Complex) * (p2 . 1) by HURWITZ:25
.= (rpoly (1,(zeta ^2))) . 1 by FIELD_9:def 2
.= 1_ F_Complex by HURWITZ:25 ;
3 in dom r by B4, ENUMSET1:def 1;
then r . 3 = (p1 . 2) * (p2 . ((2 + 1) -' 3)) by K, C, B1
.= ((rpoly (1,zeta)) . 2) * (p2 . ((2 + 1) -' 3)) by FIELD_9:def 2
.= (0. F_Complex) * (p2 . ((2 + 1) -' 3)) by HURWITZ:26 ;
then Sum r = ((0. F_Complex) + (1. F_Complex)) + (0. F_Complex) by B3, B5, B6, RLVECT_1:46
.= 1. F_Complex ;
hence (p1 *' p2) . o = q . o by C, D0, B1, COMPLFLD:def 1, GAUSSINT:13, COMPLEX1:def 4; :: thesis: verum

end;

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

then C1: i >= 2 + 1 by NAT_1:13;
then E: q . i = 0. F_Rat by FIELD_9:16
.= 0. F_Complex by GAUSSINT:13, COMPLFLD:def 1 ;
( p1 = rpoly (1,zeta) & p2 = rpoly (1,(zeta ^2)) ) by FIELD_9:def 2;
then C2: ( deg p1 = 1 & deg p2 = 1 ) by HURWITZ:27;
C3: ( 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 C2, C3, E, L, C1, XXREAL_0:2, ALGSEQ_1:8; :: thesis: verum

end;

end;

end;

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