set x = the Element of D;
<* the Element of D*> /. 1 = <* the Element of D*> /. (len <* the Element of D*>) by FINSEQ_1:39;
then <* the Element of D*> 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