theorem :: NAT_3:48

for a, b being non zero Nat holds support (pfexp a) = support (pfexp (a |^ b))