theorem :: MOEBIUS2:35

for p being Prime
for n being non zero Nat st n in FreeGen p holds
card (support (pfexp n)) <= p