set K = FAdj (F_Rat,{2-CRoot(2),zeta});
the carrier of (Polynom-Ring F_Rat) c= the carrier of (Polynom-Ring (FAdj (F_Rat,{2-CRoot(2),zeta}))) by FIELD_4:10;
then reconsider p = X^3-2 as Element of the carrier of (Polynom-Ring (FAdj (F_Rat,{2-CRoot(2),zeta}))) ;
deg p = 3 by LL, FIELD_4:20;
then reconsider p = p as non constant Element of the carrier of (Polynom-Ring (FAdj (F_Rat,{2-CRoot(2),zeta}))) by RING_4:def 4;

now :: thesis: for r being Element of F_Real
for a being Element of F_Complex st a = r holds
a |^ 3 = r |^ 3

let r be Element of F_Real; :: thesis: for a being Element of F_Complex st a = r holds
a |^ 3 = r |^ 3
let a be Element of F_Complex; :: thesis: ( a = r implies a |^ 3 = r |^ 3 )
assume A: a = r ; :: thesis: a |^ 3 = r |^ 3
B: a |^ 3 = a |^ (2 + 1)
.= (a |^ 2) * (a |^ 1) by BINOM:10
.= (a |^ (1 + 1)) * a by BINOM:8
.= ((a |^ 1) * (a |^ 1)) * a by BINOM:10
.= (a * (a |^ 1)) * a by BINOM:8
.= (a * a) * a by BINOM:8 ;
r |^ 3 = r |^ (2 + 1)
.= (r |^ 2) * (r |^ 1) by BINOM:10
.= (r |^ (1 + 1)) * r by BINOM:8
.= ((r |^ 1) * (r |^ 1)) * r by BINOM:10
.= (r * (r |^ 1)) * r by BINOM:8
.= (r * r) * r by BINOM:8 ;
hence a |^ 3 = r |^ 3 by A, B; :: thesis: verum

end;

then H: 3-CRoot(2) |^ 3 = 2 by R32;
Ext_eval (p,3-CRoot(2)) = Ext_eval (X^3-2,3-CRoot(2)) by FIELD_7:15
.= (3-CRoot(2) |^ 3) - 2 by evalext2
.= 0. F_Complex by H, COMPLFLD:def 1 ;
hence 3-CRoot(2) is FAdj (F_Rat,{2-CRoot(2),zeta}) -algebraic by FIELD_6:43; :: thesis: verum