set F = FAdj (F_Rat,{3-CRoot(2),zeta});
set K = FAdj (F_Rat,{3-CRoot(2)});
C: 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 ;
reconsider z = zeta as FAdj (F_Rat,{3-CRoot(2)}) -algebraic Element of F_Complex ;
H: deg (MinPoly (z,(FAdj (F_Rat,{3-CRoot(2)})))) = 2 by mmm, LL, FIELD_4:20;

B: now :: thesis: for o being object st o in Base z holds
o in {1,z}

let o be object ; :: thesis: ( o in Base z implies b₁ in {1,z} )
assume o in Base z ; :: thesis: b₁ in {1,z}
then consider n being Element of NAT such that
B1: ( o = z |^ n & n < deg (MinPoly (z,(FAdj (F_Rat,{3-CRoot(2)})))) ) ;
n < 1 + 1 by mmm, LL, FIELD_4:20, B1;
then n <= 1 by NAT_1:13;

per cases then ( n = 0 or n = 1 ) by NAT_1:25;

suppose n = 0 ; :: thesis: b₁ in {1,z}

then o = 1_ F_Complex by B1, BINOM:8;
then o = 1 by COMPLEX1:def 4, COMPLFLD:def 1;
hence o in {1,z} by TARSKI:def 2; :: thesis: verum

end;

suppose n = 1 ; :: thesis: b₁ in {1,z}

then o = z by B1, BINOM:8;
hence o in {1,z} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

now :: thesis: for o being object st o in {1,z} holds
o in Base z

let o be object ; :: thesis: ( o in {1,z} implies b₁ in Base z )
assume o in {1,z} ; :: thesis: b₁ in Base z

per cases then ( o = 1 or o = z ) by TARSKI:def 2;

suppose o = 1 ; :: thesis: b₁ in Base z

then o = 1_ F_Complex by COMPLEX1:def 4, COMPLFLD:def 1
.= z |^ 0 by BINOM:8 ;
hence o in Base z by H; :: thesis: verum

end;

suppose o = z ; :: thesis: b₁ in Base z

then o = z |^ 1 by BINOM:8;
hence o in Base z by H; :: thesis: verum

end;

end;

end;

then Base z = {1,z} by B, TARSKI:2;
hence {1,zeta} is Basis of (VecSp ((FAdj (F_Rat,{3-CRoot(2),zeta})),(FAdj (F_Rat,{3-CRoot(2)})))) by C, FIELD_6:65; :: thesis: verum