let seq be positive-yielding Real_Sequence; :: thesis: for k being Nat holds seq . k > 0
let k be Nat; :: thesis: seq . k > 0
dom seq = NAT by FUNCT_2:def 1;
then seq . k in rng seq by FUNCT_1:3, ORDINAL1:def 12;
hence seq . k > 0 ; :: thesis: verum