let p be Nat; :: thesis: ( p + 1 is not Prime implies ReciProducts (p + 1) = ReciProducts p )
assume p + 1 is not Prime ; :: thesis: ReciProducts (p + 1) = ReciProducts p
then SetPrimes (p + 1) = SetPrimes p by PrimesSet;
hence ReciProducts (p + 1) = ReciProducts p ; :: thesis: verum