let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is being_S-Seq & 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 being_S-Seq & 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 being_S-Seq 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: len f <= (len f) + (Index p,f) by NAT_1:11;
len f = len (Rev f) by FINSEQ_5:def 3;
then A6: (len f) - (Index p,f) <= len (Rev f) by A5, XREAL_1:22;
Index p,f <= len f by A2, Th41;
then A7: (len f) - (Index p,f) = (len f) -' (Index p,f) by XREAL_1:235;
Index p,f < len f by A2, Th41;
then A8: (Index p,f) + 1 <= len f by NAT_1:13;
then (Index p,f) + 1 < len f by A3, A4, XXREAL_0:1;
then A9: 1 < (len f) - (Index p,f) by XREAL_1:22;
1 <= (Index p,f) + 1 by NAT_1:11;
then (Index p,f) + 1 in dom f by A8, FINSEQ_3:27;
then A10: (Index p,f) + 1 in dom (Rev f) by FINSEQ_5:60;
p = (Rev (Rev f)) . ((Index p,f) + 1) by A3, FINSEQ_6:29
.= (Rev f) . (((len (Rev f)) - ((Index p,f) + 1)) + 1) by A10, FINSEQ_5:61
.= (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, A6, A9, A7, Th45;
hence ((Index p,(Rev f)) + (Index p,f)) + 1 = len f by A7; :: thesis: verum