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 Element of 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 Element of NAT st
( 1 <= i & i + 1 <= len h & h . i = p ) )
A1:
4 < len h
by GOBOARD7:36;
A2:
1 < len h
by GOBOARD7:36, XXREAL_0:2;
assume
p in rng h
; ex i being Element of NAT st
( 1 <= i & i + 1 <= len h & h . i = p )
then consider x being set such that
A3:
x in dom h
and
A4:
p = h . x
by FUNCT_1:def 5;
reconsider i = x as Element of NAT by A3;
A5:
1 <= i
by A3, FINSEQ_3:27;
set j = S_Drop i,h;
A6:
i <= len h
by A3, FINSEQ_3:27;
( 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:237, 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:34;
then
(S_Drop i,h) + 1
<= ((len h) -' 1) + 1
by A8, XREAL_1:9;
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:34, XREAL_1:237;
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:237, XXREAL_0:2;
then
i mod ((len h) -' 1) = 1
by A1, Th4, XXREAL_0:2;
then A10:
S_Drop i,
h = 1
by JORDAN4:def 1;
A11:
1
<= len h
by GOBOARD7:36, XXREAL_0:2;
then A12:
len h in dom h
by FINSEQ_3:27;
1
in dom h
by A11, FINSEQ_3:27;
then h . 1 =
h /. 1
by PARTFUN1:def 8
.=
h /. (len h)
by FINSEQ_6:def 1
.=
h . (len h)
by A12, PARTFUN1:def 8
;
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:237, XXREAL_0:2;
verum end;
end;
hence
ex i being Element of NAT st
( 1 <= i & i + 1 <= len h & h . i = p )
; verum