let n be non zero Nat; :: thesis: odd-seq n is positive-yielding
for r being Real st r in rng (odd-seq n) holds
0 < r

proof

let r be Real; :: thesis: ( r in rng (odd-seq n) implies 0 < r )
assume r in rng (odd-seq n) ; :: thesis: 0 < r
then consider x being object such that
A2: ( x in dom (odd-seq n) & r = (odd-seq n) . x ) by FUNCT_1:def 3;
reconsider x0 = x as Nat by A2;
x in Seg n by A2, Th1;
then reconsider x1 = x0 as non zero Nat by FINSEQ_1:1;
r = (2 * x1) - 1 by A2, Th2;
hence 0 < r ; :: thesis: verum

end;

hence odd-seq n is positive-yielding by PARTFUN3:def 1; :: thesis: verum