:: deftheorem defines SquarefreePart MOEBIUS3:def 6 :
for n being non zero Nat holds SquarefreePart n = n div (TSqF n);