theorem DP3: :: FIELD_15:25

for F being Field
for a being non zero Element of F
for n, m being Nat holds (anpoly (a,m)) `^ n = anpoly ((a |^ n),(n * m))