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

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