let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; :: thesis: for a being non square Element of F holds MinPoly ((sqrt a),F) = X^2- a
let a be non square Element of F; :: thesis: MinPoly ((sqrt a),F) = X^2- a
Ext_eval ((X^2- a),(sqrt a)) = 0. F by FIELD_5:17
.= 0. (embField (canHomP (X^2- a))) by FIELD_2:def 7 ;
hence MinPoly ((sqrt a),F) = X^2- a by FIELD_6:52; :: thesis: verum