theorem Th18: :: MOEBIUS1:18

for k being Nat
for n being non zero Nat st support (ppf n) c= Seg (k + 1) holds
ex m being non zero Element of NAT ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )