let p be Point of (TOP-REAL 2); :: thesis: 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; :: thesis: ( p in rng h implies ex i being Element of NAT st
( 1 <= i & i + 1 <= len h & h . i = p ) )
assume
p in rng h
; :: thesis: ex i being Element of NAT st
( 1 <= i & i + 1 <= len h & h . i = p )
then consider x being set such that
A1:
( x in dom h & p = h . x )
by FUNCT_1:def 5;
reconsider i = x as Element of NAT by A1;
set j = S_Drop i,h;
A2:
( 1 <= i & i <= len h )
by A1, FINSEQ_3:27;
A3:
4 < len h
by GOBOARD7:36;
A4:
( 1 < len h & 1 + 1 <= len h )
by GOBOARD7:36, XXREAL_0:2;
( 1 <= S_Drop i,h & (S_Drop i,h) + 1 <= len h & h . (S_Drop i,h) = p )
proof
A5:
i <= ((len h) -' 1) + 1
by A2, XREAL_1:237, XXREAL_0:2;
per cases
( i <= (len h) -' 1 or i = ((len h) -' 1) + 1 )
by A5, NAT_1:8;
suppose A6:
i <= (len h) -' 1
;
:: thesis: ( 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 A2, JORDAN4:34;
then
(S_Drop i,h) + 1
<= ((len h) -' 1) + 1
by A6, XREAL_1:9;
hence
( 1
<= S_Drop i,
h &
(S_Drop i,h) + 1
<= len h &
h . (S_Drop i,h) = p )
by A1, A2, A4, A6, JORDAN4:34, XREAL_1:237;
:: thesis: verum end; suppose A7:
i = ((len h) -' 1) + 1
;
:: thesis: ( 1 <= S_Drop i,h & (S_Drop i,h) + 1 <= len h & h . (S_Drop i,h) = p )then
i = len h
by A3, XREAL_1:237, XXREAL_0:2;
then
i mod ((len h) -' 1) = 1
by A3, Th4, XXREAL_0:2;
then A8:
S_Drop i,
h = 1
by JORDAN4:def 1;
( 1
<= len h &
len h <= len h )
by GOBOARD7:36, XXREAL_0:2;
then A9:
( 1
in dom h &
len h in dom h )
by FINSEQ_3:27;
then h . 1 =
h /. 1
by PARTFUN1:def 8
.=
h /. (len h)
by FINSEQ_6:def 1
.=
h . (len h)
by A9, PARTFUN1:def 8
;
hence
( 1
<= S_Drop i,
h &
(S_Drop i,h) + 1
<= len h &
h . (S_Drop i,h) = p )
by A1, A3, A7, A8, XREAL_1:237, XXREAL_0:2;
:: thesis: verum end;
end;
hence
ex i being Element of NAT st
( 1 <= i & i + 1 <= len h & h . i = p )
; :: thesis: verum