theorem CF1: :: FIELD_15:4

for n being non zero Nat
for p being Prime ex k, m being Nat st
( n = m * (p |^ k) & not p divides m )