set F = F_Rat ;
set M = {(1. F_Real),3-Root(2),(3-Root(2) ^2)};

B: now :: thesis: for o being object st o in Base 3-Root(2) holds
o in {(1. F_Real),3-Root(2),(3-Root(2) ^2)}

let o be object ; :: thesis: ( o in Base 3-Root(2) implies b₁ in {(1. F_Real),3-Root(2),(3-Root(2) ^2)} )
assume o in Base 3-Root(2) ; :: thesis: b₁ in {(1. F_Real),3-Root(2),(3-Root(2) ^2)}
then consider n being Element of NAT such that
B1: ( o = 3-Root(2) |^ n & n < deg (MinPoly (3-Root(2),F_Rat)) ) ;
B2: n < 2 + 1 by LL, B1, LL2, FIELD_6:52;
( n <= 2 implies not not n = 0 & ... & not n = 2 ) ;

per cases then ( n = 0 or n = 1 or n = 2 ) by B2, NAT_1:13;

suppose n = 0 ; :: thesis: b₁ in {(1. F_Real),3-Root(2),(3-Root(2) ^2)}

then o = 1_ F_Real by B1, BINOM:8;
hence o in {(1. F_Real),3-Root(2),(3-Root(2) ^2)} by ENUMSET1:def 1; :: thesis: verum

end;

suppose n = 1 ; :: thesis: b₁ in {(1. F_Real),3-Root(2),(3-Root(2) ^2)}

then o = 3-Root(2) by B1, BINOM:8;
hence o in {(1. F_Real),3-Root(2),(3-Root(2) ^2)} by ENUMSET1:def 1; :: thesis: verum

end;

suppose n = 2 ; :: thesis: b₁ in {(1. F_Real),3-Root(2),(3-Root(2) ^2)}

then o = 3-Root(2) |^ (1 + 1) by B1
.= (3-Root(2) |^ 1) * (3-Root(2) |^ 1) by BINOM:10
.= (3-Root(2) |^ 1) * 3-Root(2) by BINOM:8
.= 3-Root(2) * 3-Root(2) by BINOM:8
.= 3-Root(2) ^2 by O_RING_1:def 1 ;
hence o in {(1. F_Real),3-Root(2),(3-Root(2) ^2)} by ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

now :: thesis: for o being object st o in {(1. F_Real),3-Root(2),(3-Root(2) ^2)} holds
o in Base 3-Root(2)

let o be object ; :: thesis: ( o in {(1. F_Real),3-Root(2),(3-Root(2) ^2)} implies b₁ in Base 3-Root(2) )
assume o in {(1. F_Real),3-Root(2),(3-Root(2) ^2)} ; :: thesis: b₁ in Base 3-Root(2)

per cases then ( o = 1. F_Real or o = 3-Root(2) or o = 3-Root(2) ^2 ) by ENUMSET1:def 1;

suppose o = 1. F_Real ; :: thesis: b₁ in Base 3-Root(2)

then o = 1_ F_Real
.= 3-Root(2) |^ 0 by BINOM:8 ;
hence o in Base 3-Root(2) by LL, minpolzeta; :: thesis: verum

end;

suppose o = 3-Root(2) ; :: thesis: b₁ in Base 3-Root(2)

then o = 3-Root(2) |^ 1 by BINOM:8;
hence o in Base 3-Root(2) by LL, minpolzeta; :: thesis: verum

end;

suppose o = 3-Root(2) ^2 ; :: thesis: b₁ in Base 3-Root(2)

then o = 3-Root(2) * 3-Root(2) by O_RING_1:def 1
.= (3-Root(2) |^ 1) * 3-Root(2) by BINOM:8
.= (3-Root(2) |^ 1) * (3-Root(2) |^ 1) by BINOM:8
.= 3-Root(2) |^ (1 + 1) by BINOM:10 ;
hence o in Base 3-Root(2) by LL, minpolzeta; :: thesis: verum

end;

end;

end;

then Base 3-Root(2) = {(1. F_Real),3-Root(2),(3-Root(2) ^2)} by B, TARSKI:2;
hence {1,3-Root(2),(3-Root(2) ^2)} is Basis of (VecSp ((FAdj (F_Rat,{3-Root(2)})),F_Rat)) by FIELD_6:65; :: thesis: verum