set p = <*1*>;

{1} c= INT by Lm7, TARSKI:def 3;

then rng <*1*> c= INT by FINSEQ_1:39;

then reconsider f = <*1*> as FinSequence of INT by FINSEQ_1:def 4;

take f ; :: thesis: ( not f is empty & f is positive-yielding )

{1} c= INT by Lm7, TARSKI:def 3;

then rng <*1*> c= INT by FINSEQ_1:39;

then reconsider f = <*1*> as FinSequence of INT by FINSEQ_1:def 4;

take f ; :: thesis: ( not f is empty & f is positive-yielding )

now :: thesis: for r being Real st r in rng f holds

0 < r

hence
( not f is empty & f is positive-yielding )
by PARTFUN3:def 1; :: thesis: verum0 < r

let r be Real; :: thesis: ( r in rng f implies 0 < r )

assume r in rng f ; :: thesis: 0 < r

then r in {1} by FINSEQ_1:39;

hence 0 < r by TARSKI:def 1; :: thesis: verum

end;assume r in rng f ; :: thesis: 0 < r

then r in {1} by FINSEQ_1:39;

hence 0 < r by TARSKI:def 1; :: thesis: verum