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, Th41;
then A5: ((len f) -' (Index p,f)) + (Index p,f) = len f by XREAL_1:237;
0 + 1 <= Index p,f by A2, Th41;
then (len f) + 0 < (len f) + (Index p,f) by XREAL_1:8;
then (len f) - (Index p,f) < len f by XREAL_1:21;
then A6: (len f) -' (Index p,f) < len f by A4, XREAL_1:235;
A7: Index p,f < len f by A2, Th41;
then (Index p,f) + 1 <= len f by NAT_1:13;
then 1 <= (len f) - (Index p,f) by XREAL_1:21;
then 1 <= (len f) -' (Index p,f) by NAT_D:39;
then (len f) -' (Index p,f) in dom f by A6, FINSEQ_3:27;
then A8: (Rev f) . ((len f) -' (Index p,f)) = f . (((len f) - ((len f) -' (Index p,f))) + 1) by FINSEQ_5:61
.= f . (((len f) - ((len f) - (Index p,f))) + 1) by A7, XREAL_1:235
.= f . ((0 + (Index p,f)) + 1) ;
p in LSeg f,(Index p,f) by A2, Th42;
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:36;
then (len f) -' (Index p,f) = Index p,(Rev f) by A1, A3, A9, A10, A8, Th47, SPPOL_2:29;
hence (Index p,(Rev f)) + (Index p,f) = len f by A7, XREAL_1:237; :: thesis: verum