( <*0*> is natural-valued & not <*0*> is empty ) ;
hence ex b₁ being FinSequence st
( not b₁ is empty & b₁ is natural-valued ) ; :: thesis: verum