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 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 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 ; :: thesis: 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 )

( 1 <= i & i + 1 <= len h & h . i = p ) ; :: thesis: verum

ex i being 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 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 ; :: thesis: 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

hence
ex i being Nat st
A7:
i <= ((len h) -' 1) + 1
by A5, A6, XREAL_1:235, XXREAL_0:2;

end;per cases
( i <= (len h) -' 1 or i = ((len h) -' 1) + 1 )
by A7, NAT_1:8;

end;

suppose A8:
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 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; :: thesis: verum

end;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; :: thesis: verum

suppose A9:
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 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; :: thesis: verum

end;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; :: thesis: verum

( 1 <= i & i + 1 <= len h & h . i = p ) ; :: thesis: verum