theorem :: MOEBIUS3:63

for n being Nat holds ln . ((Partial_Product Reci-seq2) . (indexp n)) <= (Partial_Sums ReciPrime) . n