theorem GreaterProduct: :: MOEBIUS3:61

for n being Nat holds (Partial_Product Reci-seq2) . n > 0