theorem XYZb: :: REALALG3:24

for F being Field
for E being FieldExtension of F
for a being Element of E st a ^2 in F holds
for b being Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in F & c2 in F & b = c1 + ((@ ((FAdj (F,{a})),a)) * c2) )