theorem ThA: :: FIELD_16:12

for F being Field
for E being FieldExtension of F
for a being Element of E
for n being Nat holds a |^ n in the carrier of (FAdj (F,{a}))