let i be non zero Nat; :: thesis: i |-> (1 / i) is ProbFinS FinSequence of REAL
reconsider i = i as non zero Element of NAT by ORDINAL1:def 12;
A1: for k being Nat st k in dom (i |-> (1 / i)) holds
(i |-> (1 / i)) . k >= 0

proof

let k be Nat; :: thesis: ( k in dom (i |-> (1 / i)) implies (i |-> (1 / i)) . k >= 0 )
assume k in dom (i |-> (1 / i)) ; :: thesis: (i |-> (1 / i)) . k >= 0
then k in Seg i by FUNCOP_1:13;
hence (i |-> (1 / i)) . k >= 0 by FUNCOP_1:7; :: thesis: verum

end;

reconsider 1i = 1 / i as Element of REAL by XREAL_0:def 1;
reconsider ii = i |-> 1i as FinSequence of REAL ;
Sum (i |-> (1 / i)) = i * (1 / i) by RVSUM_1:80
.= 1 by XCMPLX_1:106 ;
then ii is ProbFinS by A1, MATRPROB:def 5;
hence i |-> (1 / i) is ProbFinS FinSequence of REAL ; :: thesis: verum