set F = F_Rat ;

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

let o be object ; :: thesis: ( o in Base zeta implies b₁ in {1,zeta} )
assume o in Base zeta ; :: thesis: b₁ in {1,zeta}
then consider n being Element of NAT such that
B1: ( o = zeta |^ n & n < deg (MinPoly (zeta,F_Rat)) ) ;
n < 1 + 1 by LL, B1, minpzeta;
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,zeta}

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

end;

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

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

end;

end;

end;

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

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

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

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

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

end;

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

then o = zeta |^ 1 by BINOM:8;
hence o in Base zeta by LL, minpzeta; :: thesis: verum

end;

end;

end;

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