let h be non constant standard special_circular_sequence; :: thesis: 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 & n_n_e h <= (n_n_e h) + 1 )
by NAT_1:11;
A2:
( 1 <= n_n_w h & (n_n_w h) + 1 <= len h & 1 <= n_n_e h & (n_n_e h) + 1 <= len h )
by Def10, Def12;
then
( n_n_w h <= len h & n_n_e h <= len h )
by A1, XXREAL_0:2;
then A3:
( n_n_w h in dom h & n_n_e h in dom h )
by A2, FINSEQ_3:27;
A4:
h . (n_n_w h) = W-max (L~ h)
by Def10;
A5:
h . (n_n_e h) = E-max (L~ h)
by Def12;
A6:
( h . (n_n_w h) = h /. (n_n_w h) & h . (n_n_e h) = h /. (n_n_e h) )
by A3, PARTFUN1:def 8;
thus
n_n_w h <> n_n_e h
:: thesis: verumproof
assume
n_n_w h = n_n_e h
;
:: thesis: contradiction
then A7:
W-bound (L~ h) =
(h /. (n_n_e h)) `1
by A4, A6, EUCLID:56
.=
E-bound (L~ h)
by A5, A6, EUCLID:56
;
1
<= len h
by GOBOARD7:36, XXREAL_0:2;
then
(
(h /. 1) `1 <= E-bound (L~ h) &
(h /. 1) `1 >= W-bound (L~ h) )
by Th14;
then A8:
(h /. 1) `1 = W-bound (L~ h)
by A7, XXREAL_0:1;
consider ii being
Element of
NAT such that A9:
(
ii in dom h &
(h /. ii) `1 <> (h /. 1) `1 )
by GOBOARD7:32;
A10:
( 1
<= ii &
ii <= len h )
by A9, FINSEQ_3:27;
then A11:
(h /. ii) `1 <= E-bound (L~ h)
by Th14;
(h /. ii) `1 >= W-bound (L~ h)
by A10, Th14;
hence
contradiction
by A7, A8, A9, A11, XXREAL_0:1;
:: thesis: verum
end;