theorem :: MOEBIUS3:51

for k, n being non zero Nat holds
( k ^2 divides SquarefreePart n iff k = 1 ) by Surprise, NAT_D:6;