consider f being FinSequence of ExtREAL ;
f is extreal-yielding ;
hence ex b₁ being FinSequence st b₁ is extreal-yielding ; :: thesis: verum