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

proof

let r be Real; :: thesis: ( r in rng (even-seq n) implies 0 < r )
assume r in rng (even-seq n) ; :: thesis: 0 < r
then consider x being object such that
A2: ( x in dom (even-seq n) & r = (even-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 by A2, Def1;
hence 0 < r ; :: thesis: verum

end;

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