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