not 3-Root(2) in the carrier of F_Rat ;
hence not 3-CRoot(2) is F_Rat -membered by FIELD_7:def 5; :: thesis: 3-CRoot(2) is F_Rat -algebraic
Ext_eval (X^3-2,3-CRoot(2)) = Ext_eval (X^3-2,3-Root(2)) by FIELD_7:14
.= 0. F_Complex by LL2, COMPLFLD:def 1 ;
hence 3-CRoot(2) is F_Rat -algebraic by FIELD_6:43; :: thesis: verum