( 1 |-> 0 is empty-yielding & not 1 |-> 0 is empty ) ;
hence not for b₁ being empty-yielding FinSequence holds b₁ is empty ; :: thesis: verum