theorem :: FIELD_9:61

for F being non 2 -characteristic polynomial_disjoint non quadratic_complete Field
for a being non square Element of F
for a1, a2, b1, b2 being b₁ -membered Element of (FAdj (F,{(sqrt a)})) st a1 + ((@ (sqrt a)) * b1) = a2 + ((@ (sqrt a)) * b2) holds
( a1 = a2 & b1 = b2 )