set f = <*{} *>;
<*{} *> is one-to-one by FINSEQ_3:102;
hence ex b₁ being FinSequence st
( b₁ is one-to-one & not b₁ is empty ) ; :: thesis: verum