consider d1, d2 being Element of D such that
A1: d1 <> d2 by SUBSET_1:def 7;
take f = <*d1,d2,d1*>; :: thesis: ( f is V25() & f is circular )
A2: ( f . 1 = d1 & f . 2 = d2 ) by FINSEQ_1:45;
( 1 in dom f & 2 in dom f ) by FINSEQ_1:81;
hence f is V25() by A1, A2; :: thesis: f is circular
A3: len f = 3 by FINSEQ_1:45;
thus f /. 1 = d1 by FINSEQ_4:18
.= f /. (len f) by A3, FINSEQ_4:18 ; :: according to FINSEQ_6:def 1 :: thesis: verum