let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E st not a in F & a ^2 in F holds
( {(1. E),a} is Basis of (VecSp ((FAdj (F,{a})),F)) & deg ((FAdj (F,{a})),F) = 2 )
let E be FieldExtension of F; :: thesis: for a being Element of E st not a in F & a ^2 in F holds
( {(1. E),a} is Basis of (VecSp ((FAdj (F,{a})),F)) & deg ((FAdj (F,{a})),F) = 2 )
let a be Element of E; :: thesis: ( not a in F & a ^2 in F implies ( {(1. E),a} is Basis of (VecSp ((FAdj (F,{a})),F)) & deg ((FAdj (F,{a})),F) = 2 ) )
assume AS: ( not a in F & a ^2 in F ) ; :: thesis: ( {(1. E),a} is Basis of (VecSp ((FAdj (F,{a})),F)) & deg ((FAdj (F,{a})),F) = 2 )
reconsider a1 = a as F -algebraic Element of E by AS, lemBas0;
reconsider b = a ^2 as Element of F by AS;
B: deg (MinPoly (a1,F)) = deg (X^2- b) by AS, lemBas1
.= 2 by FIELD_9:def 4 ;
Base a1 = {(1. E),a}

proof

C: now :: thesis: for o being object st o in Base a1 holds
o in {(1. E),a}

let o be object ; :: thesis: ( o in Base a1 implies b₁ in {(1. E),a} )
assume o in Base a1 ; :: thesis: b₁ in {(1. E),a}
then consider n being Element of NAT such that
D1: ( o = a1 |^ n & n < 2 ) by B;

per cases ( n = 0 or n = 1 ) by D1, NAT_1:23;

suppose n = 0 ; :: thesis: b₁ in {(1. E),a}

then o = 1_ E by D1, BINOM:8;
hence o in {(1. E),a} by TARSKI:def 2; :: thesis: verum

end;

suppose n = 1 ; :: thesis: b₁ in {(1. E),a}

then o = a by D1, BINOM:8;
hence o in {(1. E),a} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

now :: thesis: for o being object st o in {(1. E),a} holds
o in Base a1

let o be object ; :: thesis: ( o in {(1. E),a} implies b₁ in Base a1 )
assume o in {(1. E),a} ; :: thesis: b₁ in Base a1

per cases then ( o = 1. E or o = a ) by TARSKI:def 2;

suppose o = 1. E ; :: thesis: b₁ in Base a1

then o = 1_ E
.= a1 |^ 0 by BINOM:8 ;
hence o in Base a1 by B; :: thesis: verum

end;

suppose o = a ; :: thesis: b₁ in Base a1

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

end;

end;

end;

hence Base a1 = {(1. E),a} by C, TARSKI:2; :: thesis: verum

end;

hence {(1. E),a} is Basis of (VecSp ((FAdj (F,{a})),F)) by FIELD_6:65; :: thesis: deg ((FAdj (F,{a})),F) = 2
thus deg ((FAdj (F,{a})),F) = 2 by B, FIELD_6:67; :: thesis: verum