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

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

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

then
a0 is at_most_one
;
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 by FINSEQ_1:def 8; :: thesis: verum

end;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 by FINSEQ_1:def 8; :: thesis: verum

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