set f = <*a,b,a*>;
A8: len <*a,b,a*> = 3 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
.= <*a,b,a*> /. (len <*a,b,a*>) by PARTFUN1:def 6, K2 ;
hence for b₁ being FinSequence of D st b₁ = <*a,b,a*> holds
b₁ is circular ; :: thesis: verum