set f = <*1*>;
for n being Nat st n in dom <*1*> holds
<*1*> . n > 0

proof

let n be Nat; :: thesis: ( n in dom <*1*> implies <*1*> . n > 0 )
assume n in dom <*1*> ; :: thesis: <*1*> . n > 0
then n in {1} by FINSEQ_1:2, FINSEQ_1:38;
then n = 1 by TARSKI:def 1;
hence <*1*> . n > 0 ; :: thesis: verum

end;

then ( not <*1*> is empty & <*1*> is positive ) ;
hence ex b₁ being real-valued FinSequence st
( not b₁ is empty & b₁ is constant & b₁ is positive ) ; :: thesis: verum