let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f & f is weakly-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 weakly-one-to-one implies B_Cut (f,p,p) = <*p*> )
assume that
A1: p in L~ f and
A2: f is weakly-one-to-one ; :: thesis: B_Cut (f,p,p) = <*p*>
A3: 1 <= Index (p,f) by A1, JORDAN3:8;
(L_Cut (f,p)) . 1 = p by A1, JORDAN3:23;
then A4: R_Cut ((L_Cut (f,p)),p) = <*p*> by JORDAN3:def 4;
A5: Index (p,f) < len f by A1, JORDAN3:8;
then A6: (Index (p,f)) + 1 <= len f by NAT_1:13;
then A7: (Index (p,f)) + 1 in dom f by A3, SEQ_4:134;
f . (Index (p,f)) <> f . ((Index (p,f)) + 1) by A2, A5, A3;
then A8: f . (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A7, PARTFUN1:def 6;
Index (p,f) in dom f by A3, A6, SEQ_4:134;
then A9: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A8, PARTFUN1:def 6;
p in LSeg (f,(Index (p,f))) by A1, JORDAN3:9;
then p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, A6, TOPREAL1:def 3;
then LE p,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A9, JORDAN5B:9;
hence B_Cut (f,p,p) = <*p*> by A4, JORDAN3:def 7; :: thesis: verum