let f be non constant standard special_circular_sequence; :: thesis: for i, j being Element of NAT st 1 <= i & i < j & j < len f holds
f /. i <> f /. j
len f > 4 by Th36;
hence for i, j being Element of NAT st 1 <= i & i < j & j < len f holds
f /. i <> f /. j by Th37; :: thesis: verum