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:69;
then A4: 2 <= len (L_Cut f,p) by TOPREAL1:def 10;
then 1 <= len (L_Cut f,p) by XXREAL_0:2;
then 1 in dom (L_Cut f,p) by FINSEQ_3:27;
then (L_Cut f,p) /. 1 = (L_Cut f,p) . 1 by PARTFUN1:def 8
.= p by A1, JORDAN3:58 ;
hence Index p,(L_Cut f,p) = 1 by A4, JORDAN3:44; :: thesis: verum