reconsider p = X^3-2 as Polynomial of F_Complex by FIELD_4:8;
( X^3-2 is Element of the carrier of (Polynom-Ring F_Rat) & p is Element of the carrier of (Polynom-Ring F_Complex) ) by POLYNOM3:def 10;
then deg p = 3 by LL, FIELD_4:20;
then reconsider p = p as non constant Polynomial of F_Complex by RATFUNC1:def 2;
consider a being non zero Element of F_Complex, q being Ppoly of F_Complex such that
B: p = a * q by llsplit1, FIELD_4:def 5;
thus X^3-2 splits_in F_Complex by B, FIELD_4:def 5; :: thesis: ( X^3-1 splits_in F_Complex & X^2+X+1 splits_in F_Complex )
reconsider p = X^3-1 as Polynomial of F_Complex by FIELD_4:8;
( X^3-1 is Element of the carrier of (Polynom-Ring F_Rat) & p is Element of the carrier of (Polynom-Ring F_Complex) ) by POLYNOM3:def 10;
then deg p = 3 by LL, FIELD_4:20;
then reconsider p = p as non constant Polynomial of F_Complex by RATFUNC1:def 2;
consider a being non zero Element of F_Complex, q being Ppoly of F_Complex such that
B: p = a * q by llsplit1, FIELD_4:def 5;
thus X^3-1 splits_in F_Complex by B, FIELD_4:def 5; :: thesis: X^2+X+1 splits_in F_Complex
reconsider p = X^2+X+1 as Polynomial of F_Complex by FIELD_4:8;
A: deg X^2+X+1 = 2 by FIELD_9:def 4;
( X^2+X+1 is Element of the carrier of (Polynom-Ring F_Rat) & p is Element of the carrier of (Polynom-Ring F_Complex) ) by POLYNOM3:def 10;
then deg p = 2 by A, FIELD_4:20;
then reconsider p = p as non constant Polynomial of F_Complex by RATFUNC1:def 2;
consider a being non zero Element of F_Complex, q being Ppoly of F_Complex such that
B: p = a * q by llsplit1, FIELD_4:def 5;
thus X^2+X+1 splits_in F_Complex by B, FIELD_4:def 5; :: thesis: verum