reconsider z = <%1%> as XFinSequence of REAL ;

now :: thesis: for r being Real st r in rng z holds
0 < r

let r be Real; :: thesis: ( r in rng z implies 0 < r )
assume r in rng z ; :: thesis: 0 < r
then r in {1} by AFINSQ_1:33;
hence 0 < r ; :: thesis: verum

end;

then z is positive-yielding ;
hence not for b₁ being positive-yielding XFinSequence of REAL holds b₁ is empty ; :: thesis: verum