reconsider q = X^2+X+1 as Polynomial of F_Rat ;
reconsider p = (X- zeta) * (X- (zeta ^2)) as Polynomial of F_Complex by POLYNOM3:def 10;
B: X- (1. F_Complex) = rpoly (1,(1. F_Complex)) by FIELD_9:def 2;
C: X- (1. F_Rat) = rpoly (1,(1. F_Rat)) by FIELD_9:def 2;
1. F_Rat = 1. F_Complex by GAUSSINT:13, COMPLEX1:def 4, COMPLFLD:def 1;
then A: X- (1. F_Complex) = X- (1. F_Rat) by B, C, FIELD_4:21;
thus X^3-1 = (rpoly (1,(1. F_Rat))) *' q by C, lemX3, POLYNOM3:def 10
.= (rpoly (1,(1. F_Complex))) *' p by A, B, C, FIELD_4:17, lemX3a
.= (X- (1. F_Complex)) * ((X- zeta) * (X- (zeta ^2))) by B, POLYNOM3:def 10
.= ((X- (1. F_Complex)) * (X- zeta)) * (X- (zeta ^2)) by GROUP_1:def 3 ; :: thesis: verum