set F = FAdj (F_Rat,{3-CRoot(2),zeta});
set K = FAdj (F_Rat,{3-CRoot(2)});
A: deg ((FAdj (F_Rat,{3-Root(2)})),F_Rat) = 3 by LL, minpolzeta, FIELD_6:67;
B: FAdj (F_Rat,{3-CRoot(2)}) = FAdj (F_Rat,{3-Root(2)}) by mmk;
FAdj (F_Rat,{3-CRoot(2),zeta}) = FAdj (F_Rat,({3-CRoot(2)} \/ {zeta})) by ENUMSET1:1
.= FAdj ((FAdj (F_Rat,{3-CRoot(2)})),{zeta}) by FIELD_7:35 ;
then deg ((FAdj (F_Rat,{3-CRoot(2),zeta})),F_Rat) = (deg ((FAdj (F_Rat,{3-CRoot(2),zeta})),(FAdj (F_Rat,{3-CRoot(2)})))) * (deg ((FAdj (F_Rat,{3-CRoot(2)})),F_Rat)) by FIELD_7:30
.= 6 by A, B, mml ;
hence deg ((FAdj (F_Rat,{3-CRoot(2),zeta})),F_Rat) = 6 ; :: thesis: verum