let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is weakly-one-to-one implies for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds
(B_Cut (f,p,q)) /. 1 = p )
assume A1: f is weakly-one-to-one ; :: thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds
(B_Cut (f,p,q)) /. 1 = p
let p, q be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & q in L~ f implies (B_Cut (f,p,q)) /. 1 = p )
assume that
A2: p in L~ f and
A3: q in L~ f ; :: thesis: (B_Cut (f,p,q)) /. 1 = p
A4: Index (p,f) < len f by A2, JORDAN3:8;
A5: 1 <= Index (p,f) by A2, JORDAN3:8;
then A6: Index (p,f) in dom f by A4, FINSEQ_3:25;
A7: 1 <= len (L_Cut (f,p)) by A2, Th1;

per cases ( p <> q or p = q ) ;

suppose A8: p <> q ; :: thesis: (B_Cut (f,p,q)) /. 1 = p

now :: thesis: (B_Cut (f,p,q)) /. 1 = p

per cases ( ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) or ( ( not p in L~ f or not q in L~ f or not Index (p,f) < Index (q,f) ) & ( not Index (p,f) = Index (q,f) or not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ) ;

suppose A9: ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) ) ; :: thesis: (B_Cut (f,p,q)) /. 1 = p

then q in L~ (L_Cut (f,p)) by JORDAN3:29;
then (R_Cut ((L_Cut (f,p)),q)) /. 1 = (L_Cut (f,p)) /. 1 by SPRECT_3:22
.= (L_Cut (f,p)) . 1 by A7, FINSEQ_4:15
.= p by A9, JORDAN3:23 ;
hence (B_Cut (f,p,q)) /. 1 = p by A9, JORDAN3:def 7; :: thesis: verum

end;

suppose A10: ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ; :: thesis: (B_Cut (f,p,q)) /. 1 = p

then q in L~ (L_Cut (f,p)) by A2, A3, A8, JORDAN3:31;
then (R_Cut ((L_Cut (f,p)),q)) /. 1 = (L_Cut (f,p)) /. 1 by SPRECT_3:22
.= (L_Cut (f,p)) . 1 by A7, FINSEQ_4:15
.= p by A2, JORDAN3:23 ;
hence (B_Cut (f,p,q)) /. 1 = p by A10, JORDAN3:def 7; :: thesis: verum

end;

suppose A11: ( ( not p in L~ f or not q in L~ f or not Index (p,f) < Index (q,f) ) & ( not Index (p,f) = Index (q,f) or not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) ; :: thesis: (B_Cut (f,p,q)) /. 1 = p

then A12: B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by JORDAN3:def 7;

now :: thesis: (B_Cut (f,p,q)) /. 1 = p

per cases ( Index (p,f) > Index (q,f) or Index (p,f) = Index (q,f) ) by A2, A3, A11, XXREAL_0:1;

suppose Index (p,f) > Index (q,f) ; :: thesis: (B_Cut (f,p,q)) /. 1 = p

then A13: p in L~ (L_Cut (f,q)) by A2, A3, JORDAN3:29;
R_Cut ((L_Cut (f,q)),p) <> {} by JORDAN1J:44;
hence (B_Cut (f,p,q)) /. 1 = (R_Cut ((L_Cut (f,q)),p)) /. (len (R_Cut ((L_Cut (f,q)),p))) by A12, FINSEQ_5:65
.= p by A13, JORDAN1J:45 ;
:: thesis: verum

end;

suppose A14: Index (p,f) = Index (q,f) ; :: thesis: (B_Cut (f,p,q)) /. 1 = p

A15: (Index (p,f)) + 1 >= 1 by NAT_1:11;
(Index (p,f)) + 1 <= len f by A4, NAT_1:13;
then A16: (Index (p,f)) + 1 in dom f by A15, FINSEQ_3:25;
set Ls = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1)));
A17: q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, A14, JORDAN5B:29;
A18: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, JORDAN5B:29;
f . (Index (p,f)) <> f . ((Index (p,f)) + 1) by A1, A5, A4;
then f . (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A16, PARTFUN1:def 6;
then A19: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A6, PARTFUN1:def 6;
then A20: LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) is_an_arc_of f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by TOPREAL1:9;
not LE p,q, LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))),f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A11, A14, A19, JORDAN5C:17;
then LE q,p, LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))),f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A8, A20, A18, A17, JORDAN5C:14;
then A21: p in L~ (L_Cut (f,q)) by A2, A3, A8, A14, A19, JORDAN3:31, JORDAN5C:17;
R_Cut ((L_Cut (f,q)),p) <> {} by JORDAN1J:44;
hence (B_Cut (f,p,q)) /. 1 = (R_Cut ((L_Cut (f,q)),p)) /. (len (R_Cut ((L_Cut (f,q)),p))) by A12, FINSEQ_5:65
.= p by A21, JORDAN1J:45 ;
:: thesis: verum

end;

end;

end;

hence (B_Cut (f,p,q)) /. 1 = p ; :: thesis: verum

end;

end;

end;

hence (B_Cut (f,p,q)) /. 1 = p ; :: thesis: verum

end;

suppose p = q ; :: thesis: (B_Cut (f,p,q)) /. 1 = p

then B_Cut (f,p,q) = <*p*> by A1, A2, Th15;
hence (B_Cut (f,p,q)) /. 1 = p by FINSEQ_4:16; :: thesis: verum

end;

end;