set F = F_Rat ;

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

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

then o = 1_ F_Real by B1, BINOM:8;
hence o in {1,(sqrt 2)} by TARSKI:def 2; :: thesis: verum

end;

suppose n = 1 ; :: thesis: b₁ in {1,(sqrt 2)}

then o = 2-Root(2) by B1, BINOM:8;
hence o in {1,(sqrt 2)} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

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

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

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

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

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

end;

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

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

end;

end;

end;

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