let
f
be
V8
()
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