let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f & p <> f . (len f) & f is being_S-Seq holds
Index (p,(L_Cut (f,p))) = 1
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & p <> f . (len f) & f is being_S-Seq implies Index (p,(L_Cut (f,p))) = 1 )
assume that
A1: p in L~ f and
A2: p <> f . (len f) and
A3: f is being_S-Seq ; :: thesis: Index (p,(L_Cut (f,p))) = 1
L_Cut (f,p) is being_S-Seq by A1, A2, A3, JORDAN3:34;
then A4: 2 <= len (L_Cut (f,p)) by TOPREAL1:def 8;
then 1 <= len (L_Cut (f,p)) by XXREAL_0:2;
then 1 in dom (L_Cut (f,p)) by FINSEQ_3:25;
then (L_Cut (f,p)) /. 1 = (L_Cut (f,p)) . 1 by PARTFUN1:def 6
.= p by A1, JORDAN3:23 ;
hence Index (p,(L_Cut (f,p))) = 1 by A4, JORDAN3:11; :: thesis: verum