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

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