set a0 = <*1*>;
L100: rng <*1*> = {1} by FINSEQ_1:38;
then L200: <*1*> is non empty FinSequence of REAL by FINSEQ_1:def 4;
for r being Real st r in rng <*1*> holds
0 < r by L100;
then <*1*> is positive by PARTFUN3:def 1;
hence ex a being non empty FinSequence of REAL st a is positive by L200; :: thesis: verum