theorem F16: :: FIELD_16:8

for F being Field
for a being non zero Element of F
for n being Nat holds (a ") |^ n = (a |^ n) "