let h be non constant standard special_circular_sequence; n_e_n h <> n_e_s h
set i1 = n_e_n h;
set i2 = n_e_s h;
A1:
n_e_n h <= (n_e_n h) + 1
by NAT_1:11;
A2:
1 <= n_e_n h
by Def16;
(n_e_n h) + 1 <= len h
by Def16;
then
n_e_n h <= len h
by A1, XXREAL_0:2;
then
n_e_n h in dom h
by A2, FINSEQ_3:25;
then A3:
h . (n_e_n h) = h /. (n_e_n h)
by PARTFUN1:def 6;
A4:
n_e_s h <= (n_e_s h) + 1
by NAT_1:11;
A5:
h . (n_e_s h) = S-max (L~ h)
by Def14;
A6:
1 <= n_e_s h
by Def14;
(n_e_s h) + 1 <= len h
by Def14;
then
n_e_s h <= len h
by A4, XXREAL_0:2;
then
n_e_s h in dom h
by A6, FINSEQ_3:25;
then A7:
h . (n_e_s h) = h /. (n_e_s h)
by PARTFUN1:def 6;
A8:
h . (n_e_n h) = N-max (L~ h)
by Def16;
thus
n_e_n h <> n_e_s h
verumproof
assume
n_e_n h = n_e_s h
;
contradiction
then A9:
N-bound (L~ h) =
(h /. (n_e_s h)) `2
by A8, A3, EUCLID:52
.=
S-bound (L~ h)
by A5, A7, EUCLID:52
;
A10:
1
<= len h
by GOBOARD7:34, XXREAL_0:2;
then A11:
(h /. 1) `2 >= S-bound (L~ h)
by Th11;
consider ii being
Nat such that A12:
ii in dom h
and A13:
(h /. ii) `2 <> (h /. 1) `2
by GOBOARD7:31;
A14:
ii <= len h
by A12, FINSEQ_3:25;
A15:
1
<= ii
by A12, FINSEQ_3:25;
then A16:
(h /. ii) `2 <= N-bound (L~ h)
by A14, Th11;
A17:
(h /. ii) `2 >= S-bound (L~ h)
by A15, A14, Th11;
(h /. 1) `2 <= N-bound (L~ h)
by A10, Th11;
then
(h /. 1) `2 = N-bound (L~ h)
by A9, A11, XXREAL_0:1;
hence
contradiction
by A9, A13, A16, A17, XXREAL_0:1;
verum
end;