let p be Point of (TOP-REAL 2); for h being non constant standard special_circular_sequence st p in rng h holds
ex i being Nat st
( 1 <= i & i + 1 <= len h & h . i = p )
let h be non constant standard special_circular_sequence; ( p in rng h implies ex i being Nat st
( 1 <= i & i + 1 <= len h & h . i = p ) )
A1:
4 < len h
by GOBOARD7:34;
A2:
1 < len h
by GOBOARD7:34, XXREAL_0:2;
assume
p in rng h
; ex i being Nat st
( 1 <= i & i + 1 <= len h & h . i = p )
then consider x being object such that
A3:
x in dom h
and
A4:
p = h . x
by FUNCT_1:def 3;
reconsider i = x as Nat by A3;
A5:
1 <= i
by A3, FINSEQ_3:25;
set j = S_Drop (i,h);
A6:
i <= len h
by A3, FINSEQ_3:25;
( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p )
proof
A7:
i <= ((len h) -' 1) + 1
by A5, A6, XREAL_1:235, XXREAL_0:2;
per cases
( i <= (len h) -' 1 or i = ((len h) -' 1) + 1 )
by A7, NAT_1:8;
suppose A8:
i <= (len h) -' 1
;
( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p )then
S_Drop (
i,
h)
= i
by A5, JORDAN4:22;
then
(S_Drop (i,h)) + 1
<= ((len h) -' 1) + 1
by A8, XREAL_1:7;
hence
( 1
<= S_Drop (
i,
h) &
(S_Drop (i,h)) + 1
<= len h &
h . (S_Drop (i,h)) = p )
by A4, A5, A2, A8, JORDAN4:22, XREAL_1:235;
verum end; suppose A9:
i = ((len h) -' 1) + 1
;
( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p )then
i = len h
by A1, XREAL_1:235, XXREAL_0:2;
then
i mod ((len h) -' 1) = 1
by A1, Th2, XXREAL_0:2;
then A10:
S_Drop (
i,
h)
= 1
by JORDAN4:def 1;
A11:
1
<= len h
by GOBOARD7:34, XXREAL_0:2;
then A12:
len h in dom h
by FINSEQ_3:25;
1
in dom h
by A11, FINSEQ_3:25;
then h . 1 =
h /. 1
by PARTFUN1:def 6
.=
h /. (len h)
by FINSEQ_6:def 1
.=
h . (len h)
by A12, PARTFUN1:def 6
;
hence
( 1
<= S_Drop (
i,
h) &
(S_Drop (i,h)) + 1
<= len h &
h . (S_Drop (i,h)) = p )
by A4, A1, A9, A10, XREAL_1:235, XXREAL_0:2;
verum end;
end;
hence
ex i being Nat st
( 1 <= i & i + 1 <= len h & h . i = p )
; verum