theorem Th47: :: MOEBIUS1:47

for p being Prime
for n being non zero Nat holds (PFactors (p |^ n)) * <*p*> = <*p*>