let f be circular s.c.c. FinSequence of (TOP-REAL 2); :: thesis: ( len f > 4 implies for i, j being Nat st 1 < i & i < j & j <= len f holds
f /. i <> f /. j )
assume A1: len f > 4 ; :: 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
A2: 1 < i and
A3: i < j and
A4: j <= len f ; :: thesis: f /. i <> f /. j

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

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

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

end;

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

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

end;

end;