:: deftheorem defines SqF MOEBIUS2:def 4 :
for n being non zero Nat holds SqF n = Product (SqFactors n);