for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E
for i, j being Element of NAT st i < j & j < deg (MinPoly (a,F)) holds
a |^ i <> a |^ j