for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F holds the carrier of (FAdj (F,{(sqrt a)})) = { (y + ((@ (sqrt a)) * z)) where y, z is b₁ -membered Element of (FAdj (F,{(sqrt a)})) : verum }