consider x being Element of D;
<*x*> /. 1 = <*x*> /. (len <*x*>) by FINSEQ_1:56;
then <*x*> is circular by FINSEQ_6:def 1;
hence ex b₁ being FinSequence of D st
( b₁ is weakly-one-to-one & b₁ is circular & not b₁ is empty ) ; :: thesis: verum