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:21;
p .. f <> 1 by A2, A3, FINSEQ_4:19;
then A5: 1 < p .. f by A4, XXREAL_0:1;
A6: f . (p .. f) = p by A2, FINSEQ_4:19;
p .. f <= len f by A2, FINSEQ_4:21;
hence (Index (p,f)) + 1 = p .. f by A1, A5, A6, JORDAN3:12; :: thesis: verum