let h be non constant standard special_circular_sequence; :: thesis: n_s_w h <> n_s_e h
set i1 = n_s_w h;
set i2 = n_s_e h;
A1:
( n_s_w h <= (n_s_w h) + 1 & n_s_e h <= (n_s_e h) + 1 )
by NAT_1:11;
A2:
( 1 <= n_s_w h & (n_s_w h) + 1 <= len h & 1 <= n_s_e h & (n_s_e h) + 1 <= len h )
by Def9, Def11;
then
( n_s_w h <= len h & n_s_e h <= len h )
by A1, XXREAL_0:2;
then A3:
( n_s_w h in dom h & n_s_e h in dom h )
by A2, FINSEQ_3:27;
A4:
h . (n_s_w h) = W-min (L~ h)
by Def9;
A5:
h . (n_s_e h) = E-min (L~ h)
by Def11;
A6:
( h . (n_s_w h) = h /. (n_s_w h) & h . (n_s_e h) = h /. (n_s_e h) )
by A3, PARTFUN1:def 8;
thus
n_s_w h <> n_s_e h
:: thesis: verumproof
assume
n_s_w h = n_s_e h
;
:: thesis: contradiction
then A7:
W-bound (L~ h) =
(h /. (n_s_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;