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