theorem SinglePower: :: NUMBER18:74

for a being Real
for m being non zero Nat holds <*a*> |^ m = <*(a |^ m)*>