theorem :: MOEBIUS3:77

for n being Nat st n + 1 is Prime holds
ReciProducts (n + 1) = { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X }