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
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

per cases ( j < len f or j = len f ) by A3, XXREAL_0:1;

suppose j < len f ; :: thesis: f /. i <> f /. j

hence f /. i <> f /. j by A1, A2, Th36; :: thesis: verum

end;

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

then A4: f /. j = f /. 1 by FINSEQ_6:def 1;
i < len f by A2, A3, XXREAL_0:2;
hence f /. i <> f /. j by A1, A4, Th36; :: thesis: verum

end;

end;