set a0 = <*1*>;
rng <*1*> = {1} by FINSEQ_1:38;
then L250: for r being Real st r in rng <*1*> holds
0 < r ;
reconsider a0 = <*1*> as non empty positive FinSequence of REAL by FINSEQ_1:def 4, L250, PARTFUN3:def 1;
for i being Nat st 1 <= i & i <= len a0 holds
a0 . i <= 1

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len a0 implies a0 . i <= 1 )
assume that
L400: 1 <= i and
L410: i <= len a0 ; :: thesis: a0 . i <= 1
len a0 = 1 by FINSEQ_1:40;
then i = 1 by L410, L400, XXREAL_0:1;
hence a0 . i <= 1 ; :: thesis: verum

end;

then a0 is at_most_one ;
hence ex a being non empty positive FinSequence of REAL st a is at_most_one ; :: thesis: verum