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