let n be Nat; :: thesis: (Partial_Product Reci-seq2) . n > 0
for k being Nat holds Reci-seq2 . k > 0

proof

let k be Nat; :: thesis: Reci-seq2 . k > 0
Reci-seq2 . k = 1 + (1 / (primenumber k)) by My3Def;
hence Reci-seq2 . k > 0 ; :: thesis: verum

end;

hence (Partial_Product Reci-seq2) . n > 0 by SERIES_3:43; :: thesis: verum