theorem :: NAT_3:51

for a being Nat
for n being non zero Nat holds pfexp (n |^ a) = a * (pfexp n)