theorem ext1: :: FIELD_9:9

for F being Field
for E being FieldExtension of F
for a being Element of E holds FAdj (F,{a,(- a)}) = FAdj (F,{a})