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