let h be non constant standard special_circular_sequence; :: thesis:
set i1 = n_w_n h;
set i2 = n_w_s h;
A1: n_w_n h <= () + 1 by NAT_1:11;
A2: 1 <= n_w_n h by Def15;
(n_w_n h) + 1 <= len h by Def15;
then n_w_n h <= len h by ;
then n_w_n h in dom h by ;
then A3: h . () = h /. () by PARTFUN1:def 6;
A4: n_w_s h <= () + 1 by NAT_1:11;
A5: h . () = S-min (L~ h) by Def13;
A6: 1 <= n_w_s h by Def13;
(n_w_s h) + 1 <= len h by Def13;
then n_w_s h <= len h by ;
then n_w_s h in dom h by ;
then A7: h . () = h /. () by PARTFUN1:def 6;
A8: h . () = N-min (L~ h) by Def15;
thus n_w_n h <> n_w_s h :: thesis: verum
proof
assume n_w_n h = n_w_s h ; :: thesis: contradiction
then A9: N-bound (L~ h) = (h /. ()) `2 by
.= S-bound (L~ h) by ;
A10: 1 <= len h by ;
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 ;
A15: 1 <= ii by ;
then A16: (h /. ii) `2 <= N-bound (L~ h) by ;
A17: (h /. ii) `2 >= S-bound (L~ h) by ;
(h /. 1) `2 <= N-bound (L~ h) by ;
then (h /. 1) `2 = N-bound (L~ h) by ;
hence contradiction by A9, A13, A16, A17, XXREAL_0:1; :: thesis: verum
end;