theorem :: NAT_3:61

for n being non zero Nat holds Product (ppf n) = n