let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f & f is one-to-one holds
B_Cut f,p,p = <*p*>
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & f is one-to-one implies B_Cut f,p,p = <*p*> )
assume that
A1: p in L~ f and
A2: f is one-to-one ; :: thesis: B_Cut f,p,p = <*p*>
A3: Index p,f <> (Index p,f) + 1 ;
Index p,f < len f by A1, JORDAN3:41;
then A4: ( 1 <= Index p,f & (Index p,f) + 1 <= len f ) by A1, JORDAN3:41, NAT_1:13;
then A5: ( Index p,f in dom f & (Index p,f) + 1 in dom f ) by GOBOARD2:3;
p in LSeg f,(Index p,f) by A1, JORDAN3:42;
then p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A4, TOPREAL1:def 5;
then A6: LE p,p,f /. (Index p,f),f /. ((Index p,f) + 1) by A2, A3, A5, Th9, PARTFUN2:17;
(L_Cut f,p) . 1 = p by A1, JORDAN3:58;
then R_Cut (L_Cut f,p),p = <*p*> by JORDAN3:def 5;
hence B_Cut f,p,p = <*p*> by A6, JORDAN3:def 8; :: thesis: verum