theorem :: FIELD_15:24

for F being Field
for a being Element of F
for n being Nat holds (a | F) `^ n = (a |^ n) | F