set x = the Element of D;
set f = <* the Element of D*>;
<* the Element of D*> is one-to-one by FINSEQ_3:93;
hence ex b₁ being FinSequence of D st
( b₁ is one-to-one & not b₁ is empty ) ; :: thesis: verum