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 that
A1: f1 is circular and
A2: 1 <= len f1 ; :: thesis: f1 . 1 = f1 . (len f1)
A3: f1 . 1 = f1 /. 1 by A2, FINSEQ_4:15;
f1 /. 1 = f1 /. (len f1) by A1;
hence f1 . 1 = f1 . (len f1) by A2, A3, FINSEQ_4:15; :: thesis: verum