for n being Nat holds ReciProducts n c= ReciProducts (n + 1)