for i being non zero Nat holds i |-> (1 / i) is ProbFinS FinSequence of REAL