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