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