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)
for a being non zero Element of (FAdj (F,{(sqrt (DC p))}))
for b, c being Element of (FAdj (F,{(sqrt (DC p))})) st p = <%c,b,a%> holds
( Root1 p = ((- b) + (RootDC p)) * ((2 '*' a) ") & Root2 p = ((- b) - (RootDC p)) * ((2 '*' a) ") )