theorem :: FIELD_9:54
for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds MinPoly ((sqrt a),F) = X^2- a by m30;