let f be V8() 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

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