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