let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p = f . ((Index (p,f)) + 1) & p <> f . (len f) holds
((Index (p,(Rev f))) + (Index (p,f))) + 1 = len f
let p be Point of (TOP-REAL 2); :: thesis: ( f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p = f . ((Index (p,f)) + 1) & p <> f . (len f) implies ((Index (p,(Rev f))) + (Index (p,f))) + 1 = len f )
assume that
A1: ( f is poorly-one-to-one & f is unfolded & f is s.n.c. ) and
A2: p in L~ f and
A3: p = f . ((Index (p,f)) + 1) and
A4: p <> f . (len f) ; :: thesis: ((Index (p,(Rev f))) + (Index (p,f))) + 1 = len f
A5: Rev f is s.n.c. by A1, SPPOL_2:35;
A6: len f = len (Rev f) by FINSEQ_5:def 3;
len f <= (len f) + (Index (p,f)) by NAT_1:11;
then A7: (len f) - (Index (p,f)) <= len (Rev f) by A6, XREAL_1:20;
Index (p,f) <= len f by A2, JORDAN3:8;
then A8: (len f) - (Index (p,f)) = (len f) -' (Index (p,f)) by XREAL_1:233;
Index (p,f) < len f by A2, JORDAN3:8;
then A9: (Index (p,f)) + 1 <= len f by NAT_1:13;
then (Index (p,f)) + 1 < len f by A3, A4, XXREAL_0:1;
then A10: 1 < (len f) - (Index (p,f)) by XREAL_1:20;
1 <= (Index (p,f)) + 1 by NAT_1:11;
then (Index (p,f)) + 1 in dom f by A9, FINSEQ_3:25;
then A11: (Index (p,f)) + 1 in dom (Rev f) by FINSEQ_5:57;
p = (Rev (Rev f)) . ((Index (p,f)) + 1) by A3
.= (Rev f) . (((len (Rev f)) - ((Index (p,f)) + 1)) + 1) by A11, FINSEQ_5:58
.= (Rev f) . ((len (Rev f)) - (Index (p,f)))
.= (Rev f) . ((len f) - (Index (p,f))) by FINSEQ_5:def 3 ;
then (Index (p,(Rev f))) + 1 = (len f) -' (Index (p,f)) by A1, A5, A7, A10, A8, Th18, SPPOL_2:28;
hence ((Index (p,(Rev f))) + (Index (p,f))) + 1 = len f by A8; :: thesis: verum