set f = <*a,b,a*>;

A8: len <*a,b,a*> = 3 by FINSEQ_1:45;

A1: <*a,b,a*> . 3 = a by FINSEQ_1:45;

K1: 1 in dom <*a,b,a*> by A8, FINSEQ_3:25;

K2: len <*a,b,a*> in dom <*a,b,a*> by FINSEQ_3:25, A8;

<*a,b,a*> /. 1 = <*a,b,a*> . 1 by PARTFUN1:def 6, K1

.= <*a,b,a*> . (len <*a,b,a*>) by A8, FINSEQ_1:45, A1

.= <*a,b,a*> /. (len <*a,b,a*>) by PARTFUN1:def 6, K2 ;

hence for b_{1} being FinSequence of D st b_{1} = <*a,b,a*> holds

b_{1} is circular
; :: thesis: verum

A8: len <*a,b,a*> = 3 by FINSEQ_1:45;

A1: <*a,b,a*> . 3 = a by FINSEQ_1:45;

K1: 1 in dom <*a,b,a*> by A8, FINSEQ_3:25;

K2: len <*a,b,a*> in dom <*a,b,a*> by FINSEQ_3:25, A8;

<*a,b,a*> /. 1 = <*a,b,a*> . 1 by PARTFUN1:def 6, K1

.= <*a,b,a*> . (len <*a,b,a*>) by A8, FINSEQ_1:45, A1

.= <*a,b,a*> /. (len <*a,b,a*>) by PARTFUN1:def 6, K2 ;

hence for b

b