:: deftheorem defines Root2 FIELD_9:def 25 :
for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for p being quadratic non DC-square Element of the carrier of (Polynom-Ring F) holds Root2 p = ((- (@ ((p . 1),(FAdj (F,{(sqrt (DC p))}))))) - (RootDC p)) * ((2 '*' (@ ((p . 2),(FAdj (F,{(sqrt (DC p))}))))) ");