consider d1, d2 being Element of D such that
A1: d1 <> d2 by YELLOW_8:def 1;
take f = <*d1,d2,d1*>; :: thesis: ( not f is constant & f is circular )
A2: ( f . 1 = d1 & f . 2 = d2 ) by FINSEQ_1:62;
( 1 in dom f & 2 in dom f ) by TOPREAL3:6;
hence not f is constant by A1, A2, SEQM_3:def 15; :: thesis: f is circular
A3: len f = 3 by FINSEQ_1:62;
thus f /. 1 = d1 by FINSEQ_4:27
.= f /. (len f) by A3, FINSEQ_4:27 ; :: according to FINSEQ_6:def 1 :: thesis: verum