let f be V8() standard special_circular_sequence; :: thesis: for i, j being Nat st 1 < i & i < j & j <= len f holds

f /. i <> f /. j

let i, j be Nat; :: thesis: ( 1 < i & i < j & j <= len f implies f /. i <> f /. j )

assume that

A1: 1 < i and

A2: i < j and

A3: j <= len f ; :: thesis: f /. i <> f /. j

f /. i <> f /. j

let i, j be Nat; :: thesis: ( 1 < i & i < j & j <= len f implies f /. i <> f /. j )

assume that

A1: 1 < i and

A2: i < j and

A3: j <= len f ; :: thesis: f /. i <> f /. j