for n being non zero Nat ex k being Element of NAT st support (ppf n) c= Seg k