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 rng f & p <> f . 1 holds
(Index p,f) + 1 = p .. f
let p be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p in rng f & p <> f . 1 implies (Index p,f) + 1 = p .. f )
assume that
A1: f is being_S-Seq and
A2: p in rng f and
A3: p <> f . 1 ; :: thesis: (Index p,f) + 1 = p .. f
A4: 1 <= p .. f by A2, FINSEQ_4:31;
p .. f <> 1 by A2, A3, FINSEQ_4:29;
then A5: 1 < p .. f by A4, XXREAL_0:1;
A6: f . (p .. f) = p by A2, FINSEQ_4:29;
p .. f <= len f by A2, FINSEQ_4:31;
hence (Index p,f) + 1 = p .. f by A1, A5, A6, JORDAN3:45; :: thesis: verum