:: deftheorem defines Base FIELD_6:def 8 :
for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E holds Base a = { (a |^ n) where n is Element of NAT : n < deg (MinPoly (a,F)) } ;