:: deftheorem defines sqrt FIELD_9:def 21 :
for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds sqrt a = KrRootP (X^2- a);