let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is unfolded & 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 is unfolded )
assume A1: ( f is unfolded & 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 is unfolded
let p, q be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & q in L~ f implies B_Cut f,p,q is unfolded )
assume A2: ( p in L~ f & q in L~ f ) ; :: thesis: B_Cut f,p,q is unfolded
then A3: ( 1 <= Index p,f & Index p,f < len f ) by JORDAN3:41;
then Index p,f in Seg (len f) by FINSEQ_1:3;
then A4: Index p,f in dom f by FINSEQ_1:def 3;

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

suppose A5: p <> q ; :: thesis: B_Cut f,p,q is unfolded

now

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 & q in L~ f & Index p,f < Index q,f ) & not ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) ) ;

suppose A6: ( p in L~ f & q in L~ f & Index p,f < Index q,f ) ; :: thesis: B_Cut f,p,q is unfolded

then A7: q in L~ (L_Cut f,p) by JORDAN3:64;
L_Cut f,p is unfolded by A1, A2, Th32;
then R_Cut (L_Cut f,p),q is unfolded by A7, Th33;
hence B_Cut f,p,q is unfolded by A6, JORDAN3:def 8; :: thesis: verum

end;

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

then A9: q in L~ (L_Cut f,p) by A2, A5, JORDAN3:66;
L_Cut f,p is unfolded by A1, A2, Th32;
then R_Cut (L_Cut f,p),q is unfolded by A9, Th33;
hence B_Cut f,p,q is unfolded by A8, JORDAN3:def 8; :: thesis: verum

end;

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

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

A12: now

per cases ( Index q,f < Index p,f or Index q,f = Index p,f ) by A2, A10, XXREAL_0:1;

suppose Index q,f < Index p,f ; :: thesis: p in L~ (L_Cut f,q)

hence p in L~ (L_Cut f,q) by A2, JORDAN3:64; :: thesis: verum

end;

suppose A13: Index q,f = Index p,f ; :: thesis: p in L~ (L_Cut f,q)

set Ls = LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1));
A14: (Index p,f) + 1 <= len f by A3, NAT_1:13;
(Index p,f) + 1 >= 1 by NAT_1:11;
then (Index p,f) + 1 in Seg (len f) by A14, FINSEQ_1:3;
then A15: (Index p,f) + 1 in dom f by FINSEQ_1:def 3;
f . (Index p,f) <> f . ((Index p,f) + 1) by A1, A3, Def2;
then f . (Index p,f) <> f /. ((Index p,f) + 1) by A15, PARTFUN1:def 8;
then A16: f /. (Index p,f) <> f /. ((Index p,f) + 1) by A4, PARTFUN1:def 8;
then A17: 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:15;
A18: not LE p,q, LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)),f /. (Index p,f),f /. ((Index p,f) + 1) by A10, A13, A16, JORDAN5C:17;
A19: p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A2, JORDAN5B:32;
q in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A2, A13, JORDAN5B:32;
then LE q,p, LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)),f /. (Index p,f),f /. ((Index p,f) + 1) by A5, A17, A18, A19, JORDAN5C:14;
hence p in L~ (L_Cut f,q) by A2, A5, A13, A16, JORDAN3:66, JORDAN5C:17; :: thesis: verum

end;

end;

end;

L_Cut f,q is unfolded by A1, A2, Th32;
then R_Cut (L_Cut f,q),p is unfolded by A12, Th33;
hence B_Cut f,p,q is unfolded by A11, SPPOL_2:29; :: thesis: verum

end;

end;

end;

hence B_Cut f,p,q is unfolded ; :: thesis: verum

end;

suppose p = q ; :: thesis: B_Cut f,p,q is unfolded

then B_Cut f,p,q = <*p*> by A1, A2, Th15;
then len (B_Cut f,p,q) = 1 by FINSEQ_1:56;
hence B_Cut f,p,q is unfolded by SPPOL_2:27; :: thesis: verum

end;

end;