theorem ThBas: :: REALALG3:22

for F being Field
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 )