theorem Th16: :: ENTROPY1:16

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