theorem XYZc: :: REALALG3:25

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