theorem Th14: :: MOEBIUS1:14

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