consider f being FinSequence of REAL ;
f is real-valued ;
hence ex b₁ being FinSequence st b₁ is real-valued ; :: thesis: verum