let f be FinSequence of (); :: thesis: for p being Point of () st f is unfolded & f is s.n.c. & p in L~ f & p <> f . ((Index (p,f)) + 1) holds
(Index (p,(Rev f))) + (Index (p,f)) = len f

let p be Point of (); :: thesis: ( f is unfolded & f is s.n.c. & p in L~ f & p <> f . ((Index (p,f)) + 1) implies (Index (p,(Rev f))) + (Index (p,f)) = len f )
assume that
A1: ( f is unfolded & f is s.n.c. ) and
A2: p in L~ f and
A3: p <> f . ((Index (p,f)) + 1) ; :: thesis: (Index (p,(Rev f))) + (Index (p,f)) = len f
A4: Index (p,f) < len f by ;
then A5: ((len f) -' (Index (p,f))) + (Index (p,f)) = len f by XREAL_1:235;
0 + 1 <= Index (p,f) by ;
then (len f) + 0 < (len f) + (Index (p,f)) by XREAL_1:6;
then (len f) - (Index (p,f)) < len f by XREAL_1:19;
then A6: (len f) -' (Index (p,f)) < len f by ;
A7: Index (p,f) < len f by ;
then (Index (p,f)) + 1 <= len f by NAT_1:13;
then 1 <= (len f) - (Index (p,f)) by XREAL_1:19;
then 1 <= (len f) -' (Index (p,f)) by NAT_D:39;
then (len f) -' (Index (p,f)) in dom f by ;
then A8: (Rev f) . ((len f) -' (Index (p,f))) = f . (((len f) - ((len f) -' (Index (p,f)))) + 1) by FINSEQ_5:58
.= f . (((len f) - ((len f) - (Index (p,f)))) + 1) by
.= f . ((0 + (Index (p,f))) + 1) ;
p in LSeg (f,(Index (p,f))) by ;
then A9: p in LSeg ((Rev f),((len f) -' (Index (p,f)))) by ;
len f = len (Rev f) by FINSEQ_5:def 3;
then A10: ((len f) -' (Index (p,f))) + 1 <= len (Rev f) by ;
Rev f is s.n.c. by ;
then (len f) -' (Index (p,f)) = Index (p,(Rev f)) by ;
hence (Index (p,(Rev f))) + (Index (p,f)) = len f by ; :: thesis: verum