let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; :: thesis: for a being non square Element of F holds {(1. F),(sqrt a)} is Basis of (VecSp ((FAdj (F,{(sqrt a)})),F))
let a be non square Element of F; :: thesis: {(1. F),(sqrt a)} is Basis of (VecSp ((FAdj (F,{(sqrt a)})),F))
Base (sqrt a) = {(1. F),(sqrt a)} by qbase1;
hence {(1. F),(sqrt a)} is Basis of (VecSp ((FAdj (F,{(sqrt a)})),F)) by FIELD_6:65; :: thesis: verum