let i be non empty Nat; :: thesis: i |-> (1 / i) is ProbFinS FinSequence of REAL
reconsider i = i as non empty Element of NAT by ORDINAL1:def 13;
A1: Sum (i |-> (1 / i)) = i * (1 / i) by RVSUM_1:110
.= 1 by XCMPLX_1:107 ;
for k being Element of NAT st k in dom (i |-> (1 / i)) holds
(i |-> (1 / i)) . k >= 0

proof

let k be Element of NAT ; :: thesis: ( k in dom (i |-> (1 / i)) implies (i |-> (1 / i)) . k >= 0 )
assume A2: k in dom (i |-> (1 / i)) ; :: thesis: (i |-> (1 / i)) . k >= 0
k in Seg i by A2, FUNCOP_1:19;
hence (i |-> (1 / i)) . k >= 0 by FUNCOP_1:13; :: thesis: verum

end;

hence i |-> (1 / i) is ProbFinS FinSequence of REAL by A1, MATRPROB:def 5; :: thesis: verum