let f be constant standard special_circular_sequence; :: thesis: for i being Nat st 1 < i & i <= len f & f /. i = f /. 1 holds
i = len f
let i be Nat; :: thesis: ( 1 < i & i <= len f & f /. i = f /. 1 implies i = len f )
assume that
A1: 1 < i and
A2: i <= len f and
A3: f /. i = f /. 1 ; :: thesis: i = len f
assume i <> len f ; :: thesis: contradiction
then i < len f by A2, XXREAL_0:1;
hence contradiction by A1, A3, Th36; :: thesis: verum