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