:: deftheorem defines ReciProducts MOEBIUS3:def 11 :
for n being Nat holds ReciProducts n = { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : verum } ;