set K = FAdj (F_Rat,{3-CRoot(2)});
the carrier of (Polynom-Ring F_Rat) c= the carrier of (Polynom-Ring (FAdj (F_Rat,{3-CRoot(2)})))
by FIELD_4:10;
then reconsider p = X^2+X+1 as Element of the carrier of (Polynom-Ring (FAdj (F_Rat,{3-CRoot(2)}))) ;
A: 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
;
deg p = 2
by LL, FIELD_4:20;
hence
deg ((FAdj (F_Rat,{3-CRoot(2),zeta})),(FAdj (F_Rat,{3-CRoot(2)}))) = 2
by A, mmm, FIELD_6:67; verum