:: deftheorem defines TSqF MOEBIUS2:def 9 :
for n being non zero Nat holds TSqF n = Product (TSqFactors n);