let f be constant standard special_circular_sequence; :: thesis: for i, j being Nat st 1 <= i & i < j & j < len f holds
f /. i <> f /. j
len f > 4 by Th34;
hence for i, j being Nat st 1 <= i & i < j & j < len f holds
f /. i <> f /. j by Th35; :: thesis: verum