let f be circular s.c.c. FinSequence of (); :: 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 and
A5: f /. i = f /. j ; :: thesis: contradiction
A6: j + 1 <= len f by ;
A7: ( i + 1 <= j & i <> 0 ) by ;
1 <= j by ;
then A8: f /. j in LSeg (f,j) by ;
A9: i < len f by ;
then i + 1 <= len f by NAT_1:13;
then A10: f /. i in LSeg (f,i) by ;
( i <= 2 implies not not i = 0 & ... & not i = 2 ) ;
per cases then ( ( i + 1 = j & i = 1 ) or ( i + 1 = j & i = 1 + 1 ) or i > 1 + 1 or ( i + 1 < j & i <> 1 ) or ( i + 1 < j & j + 1 <> len f ) or ( i + 1 < j & i = 1 & j + 1 = len f ) ) by ;
suppose that A11: i + 1 = j and
A12: i = 1 ; :: thesis: contradiction
A13: ((len f) -' 1) + 1 = len f by ;
(j + 1) + 1 < len f by A1, A11, A12;
then A14: j + 1 < (len f) -' 1 by ;
(len f) -' 1 < len f by ;
then LSeg (f,j) misses LSeg (f,((len f) -' 1)) by ;
then A15: (LSeg (f,j)) /\ (LSeg (f,((len f) -' 1))) = {} by XBOOLE_0:def 7;
A16: f /. i = f /. (len f) by ;
1 + 1 <= len f by ;
then 1 <= (len f) -' 1 by ;
then f /. i in LSeg (f,((len f) -' 1)) by ;
hence contradiction by A5, A8, A15, XBOOLE_0:def 4; :: thesis: verum
end;
suppose that A17: i + 1 = j and
A18: i = 1 + 1 ; :: thesis: contradiction
A19: (i -' 1) + 1 = i by ;
j + 1 < len f by A1, A17, A18;
then LSeg (f,(i -' 1)) misses LSeg (f,j) by ;
then A20: (LSeg (f,(i -' 1))) /\ (LSeg (f,j)) = {} by XBOOLE_0:def 7;
f /. i in LSeg (f,(i -' 1)) by ;
hence contradiction by A5, A8, A20, XBOOLE_0:def 4; :: thesis: verum
end;
suppose A21: i > 1 + 1 ; :: thesis: contradiction
A22: (i -' 1) + 1 = i by ;
then A23: 1 < i -' 1 by ;
then LSeg (f,(i -' 1)) misses LSeg (f,j) by ;
then A24: (LSeg (f,(i -' 1))) /\ (LSeg (f,j)) = {} by XBOOLE_0:def 7;
f /. i in LSeg (f,(i -' 1)) by ;
hence contradiction by A5, A8, A24, XBOOLE_0:def 4; :: thesis: verum
end;
suppose that A25: i + 1 < j and
A26: i <> 1 ; :: thesis: contradiction
end;
suppose that A27: i + 1 < j and
A28: j + 1 <> len f ; :: thesis: contradiction
end;
suppose that A29: i + 1 < j and
A30: i = 1 and
A31: j + 1 = len f ; :: thesis: contradiction
A32: j < len f by ;
A33: (j -' 1) + 1 = j by ;
then A34: i + 1 <= j -' 1 by ;
i + 1 <> j -' 1 by A1, A30, A31, A33;
then i + 1 < j -' 1 by ;
then LSeg (f,1) misses LSeg (f,(j -' 1)) by ;
then A35: (LSeg (f,1)) /\ (LSeg (f,(j -' 1))) = {} by XBOOLE_0:def 7;
1 <= j -' 1 by ;
then f /. j in LSeg (f,(j -' 1)) by ;
hence contradiction by A5, A10, A30, A35, XBOOLE_0:def 4; :: thesis: verum
end;
end;