theorem :: MOEBIUS3:76

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