let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) 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 (TOP-REAL 2); :: 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 A2, Th8;

then A5: ((len f) -' (Index (p,f))) + (Index (p,f)) = len f by XREAL_1:235;

0 + 1 <= Index (p,f) by A2, Th8;

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 A4, XREAL_1:233;

A7: Index (p,f) < len f by A2, Th8;

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 A6, FINSEQ_3:25;

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 A7, XREAL_1:233

.= f . ((0 + (Index (p,f))) + 1) ;

p in LSeg (f,(Index (p,f))) by A2, Th9;

then A9: p in LSeg ((Rev f),((len f) -' (Index (p,f)))) by A5, SPPOL_2:2;

len f = len (Rev f) by FINSEQ_5:def 3;

then A10: ((len f) -' (Index (p,f))) + 1 <= len (Rev f) by A6, NAT_1:13;

Rev f is s.n.c. by A1, SPPOL_2:35;

then (len f) -' (Index (p,f)) = Index (p,(Rev f)) by A1, A3, A9, A10, A8, Th14, SPPOL_2:28;

hence (Index (p,(Rev f))) + (Index (p,f)) = len f by A7, XREAL_1:235; :: thesis: verum

(Index (p,(Rev f))) + (Index (p,f)) = len f

let p be Point of (TOP-REAL 2); :: 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 A2, Th8;

then A5: ((len f) -' (Index (p,f))) + (Index (p,f)) = len f by XREAL_1:235;

0 + 1 <= Index (p,f) by A2, Th8;

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 A4, XREAL_1:233;

A7: Index (p,f) < len f by A2, Th8;

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 A6, FINSEQ_3:25;

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 A7, XREAL_1:233

.= f . ((0 + (Index (p,f))) + 1) ;

p in LSeg (f,(Index (p,f))) by A2, Th9;

then A9: p in LSeg ((Rev f),((len f) -' (Index (p,f)))) by A5, SPPOL_2:2;

len f = len (Rev f) by FINSEQ_5:def 3;

then A10: ((len f) -' (Index (p,f))) + 1 <= len (Rev f) by A6, NAT_1:13;

Rev f is s.n.c. by A1, SPPOL_2:35;

then (len f) -' (Index (p,f)) = Index (p,(Rev f)) by A1, A3, A9, A10, A8, Th14, SPPOL_2:28;

hence (Index (p,(Rev f))) + (Index (p,f)) = len f by A7, XREAL_1:235; :: thesis: verum