theorem qbase4: :: FIELD_9:59

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds {(1. F),(sqrt a)} is Basis of (VecSp ((FAdj (F,{(sqrt a)})),F))