set d = the Element of D;
take <* the Element of D*> ; :: thesis: ( <* the Element of D*> is circular & <* the Element of D*> is 1 -element )
<* the Element of D*> /. 1 = <* the Element of D*> /. (len <* the Element of D*>) by FINSEQ_1:39;
hence <* the Element of D*> is circular by Def1; :: thesis: <* the Element of D*> is 1 -element
thus <* the Element of D*> is 1 -element ; :: thesis: verum