for n being Nat holds 0 <= ReciPrime . n
proof
let n be Nat; :: thesis: 0 <= ReciPrime . n
ReciPrime . n in rng ReciPrime by FUNCT_2:4, ORDINAL1:def 12;
hence 0 <= ReciPrime . n by PARTFUN3:def 4; :: thesis: verum
end;
hence for b1 being Real_Sequence st b1 = Partial_Sums ReciPrime holds
b1 is non-decreasing by SERIES_1:16; :: thesis: verum