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 12;
A1: 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 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;

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