let p be Point of (); :: 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 ;
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 ;
set j = S_Drop (i,h);
A6: i <= len h by ;
( 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 ;
per cases ( i <= (len h) -' 1 or i = ((len h) -' 1) + 1 ) by ;
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 ;
then (S_Drop (i,h)) + 1 <= ((len h) -' 1) + 1 by ;
hence ( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p ) by ; :: thesis: verum
end;
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 ;
then i mod ((len h) -' 1) = 1 by ;
then A10: S_Drop (i,h) = 1 by JORDAN4:def 1;
A11: 1 <= len h by ;
then A12: len h in dom h by FINSEQ_3:25;
1 in dom h by ;
then h . 1 = h /. 1 by PARTFUN1:def 6
.= h /. (len h) by FINSEQ_6:def 1
.= h . (len h) by ;
hence ( 1 <= S_Drop (i,h) & (S_Drop (i,h)) + 1 <= len h & h . (S_Drop (i,h)) = p ) by ; :: thesis: verum
end;
end;
end;
hence ex i being Nat st
( 1 <= i & i + 1 <= len h & h . i = p ) ; :: thesis: verum