let D be non empty set ; :: thesis: for f1 being FinSequence of D st f1 is circular & 1 <= len f1 holds
f1 . 1 = f1 . (len f1)
let f1 be FinSequence of D; :: thesis: ( f1 is circular & 1 <= len f1 implies f1 . 1 = f1 . (len f1) )
assume A1: ( f1 is circular & 1 <= len f1 ) ; :: thesis: f1 . 1 = f1 . (len f1)
then A2: f1 /. 1 = f1 /. (len f1) by FINSEQ_6:def 1;
f1 . 1 = f1 /. 1 by A1, FINSEQ_4:24;
hence f1 . 1 = f1 . (len f1) by A1, A2, FINSEQ_4:24; :: thesis: verum