let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is unfolded implies for p being Point of (TOP-REAL 2) st p in L~ f holds
L_Cut f,p is unfolded )
assume A1: f is unfolded ; :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
L_Cut f,p is unfolded
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies L_Cut f,p is unfolded )
A2: mid f,((Index p,f) + 1),(len f) is unfolded by A1, Th28;
assume A3: p in L~ f ; :: thesis: L_Cut f,p is unfolded
then A4: p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by JORDAN5B:32;
Index p,f < len f by A3, JORDAN3:41;
then A5: ((Index p,f) + 1) + 0 <= len f by NAT_1:13;
len f <> 0 by A3, TOPREAL1:28;
then len f > 0 by NAT_1:3;
then A6: len f >= 0 + 1 by NAT_1:13;
then A7: len f in dom f by FINSEQ_3:27;
A8: 1 <= Index p,f by A3, JORDAN3:41;
then A9: LSeg f,(Index p,f) = LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A5, TOPREAL1:def 5;
A10: 1 < (Index p,f) + 1 by A8, NAT_1:13;
then A11: (Index p,f) + 1 in dom f by A5, FINSEQ_3:27;
then A12: (mid f,((Index p,f) + 1),(len f)) /. 1 = f /. ((Index p,f) + 1) by A7, SPRECT_2:12;

per cases ( ((Index p,f) + 1) + 1 <= len f or ((Index p,f) + 1) + 1 > len f ) ;

suppose A13: ((Index p,f) + 1) + 1 <= len f ; :: thesis: L_Cut f,p is unfolded

then LSeg f,((Index p,f) + 1) = LSeg (f /. ((Index p,f) + 1)),(f /. ((Index p,f) + (1 + 1))) by A10, TOPREAL1:def 5;
then A14: (LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1))) /\ (LSeg (f /. ((Index p,f) + 1)),(f /. ((Index p,f) + (1 + 1)))) = {(f /. ((Index p,f) + 1))} by A1, A8, A9, A13, TOPREAL1:def 8;
A15: (len f) - ((Index p,f) + 1) >= 0 by A5, XREAL_1:21;
(Index p,f) + (1 + 1) <= len f by A13;
then A16: 2 <= (len f) - (Index p,f) by XREAL_1:21;
A17: f /. ((Index p,f) + 1) in LSeg (f /. ((Index p,f) + 1)),(f /. ((Index p,f) + (1 + 1))) by RLTOPSP1:69;
f /. ((Index p,f) + 1) in LSeg p,(f /. ((Index p,f) + 1)) by RLTOPSP1:69;
then f /. ((Index p,f) + 1) in (LSeg p,(f /. ((Index p,f) + 1))) /\ (LSeg (f /. ((Index p,f) + 1)),(f /. ((Index p,f) + (1 + 1)))) by A17, XBOOLE_0:def 4;
then A18: {(f /. ((Index p,f) + 1))} c= (LSeg p,(f /. ((Index p,f) + 1))) /\ (LSeg (f /. ((Index p,f) + 1)),(f /. ((Index p,f) + (1 + 1)))) by ZFMISC_1:37;
(2 + ((Index p,f) + 1)) - 1 = ((Index p,f) + 1) + 1 ;
then A19: (2 + ((Index p,f) + 1)) - 1 >= 0 by NAT_1:2;
A20: len (mid f,((Index p,f) + 1),(len f)) = ((len f) -' ((Index p,f) + 1)) + 1 by A6, A10, A5, FINSEQ_6:124
.= ((len f) - ((Index p,f) + 1)) + 1 by A15, XREAL_0:def 2
.= (len f) - (Index p,f) ;
then 2 in dom (mid f,((Index p,f) + 1),(len f)) by A16, FINSEQ_3:27;
then (mid f,((Index p,f) + 1),(len f)) /. 2 = f /. ((2 + ((Index p,f) + 1)) -' 1) by A5, A11, A7, SPRECT_2:7
.= f /. ((Index p,f) + (1 + 1)) by A19, XREAL_0:def 2 ;
then A21: LSeg (mid f,((Index p,f) + 1),(len f)),1 = LSeg (f /. ((Index p,f) + 1)),(f /. ((Index p,f) + (1 + 1))) by A12, A20, A16, TOPREAL1:def 5;
f /. ((Index p,f) + 1) in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by RLTOPSP1:69;
then (LSeg p,(f /. ((Index p,f) + 1))) /\ (LSeg (f /. ((Index p,f) + 1)),(f /. ((Index p,f) + (1 + 1)))) c= {(f /. ((Index p,f) + 1))} by A4, A14, TOPREAL1:12, XBOOLE_1:26;
then A22: (LSeg p,(f /. ((Index p,f) + 1))) /\ (LSeg (f /. ((Index p,f) + 1)),(f /. ((Index p,f) + (1 + 1)))) = {(f /. ((Index p,f) + 1))} by A18, XBOOLE_0:def 10;

now

per cases ( p <> f . ((Index p,f) + 1) or p = f . ((Index p,f) + 1) ) ;

suppose p <> f . ((Index p,f) + 1) ; :: thesis: L_Cut f,p is unfolded

then L_Cut f,p = <*p*> ^ (mid f,((Index p,f) + 1),(len f)) by JORDAN3:def 4;
hence L_Cut f,p is unfolded by A1, A12, A21, A22, Th28, SPPOL_2:30; :: thesis: verum

end;

suppose p = f . ((Index p,f) + 1) ; :: thesis: L_Cut f,p is unfolded

hence L_Cut f,p is unfolded by A2, JORDAN3:def 4; :: thesis: verum

end;

end;

end;

hence L_Cut f,p is unfolded ; :: thesis: verum

end;

suppose A23: ((Index p,f) + 1) + 1 > len f ; :: thesis: L_Cut f,p is unfolded

A24: ( (Index p,f) + 1 < len f or (Index p,f) + 1 = len f ) by A5, XXREAL_0:1;

now

per cases ( p <> f . ((Index p,f) + 1) or p = f . ((Index p,f) + 1) ) ;

suppose p <> f . ((Index p,f) + 1) ; :: thesis: L_Cut f,p is unfolded

then L_Cut f,p = <*p*> ^ (mid f,(len f),(len f)) by A23, A24, JORDAN3:def 4, NAT_1:13
.= <*p*> ^ <*(f /. (len f))*> by A6, JORDAN4:27
.= <*p,(f /. (len f))*> by FINSEQ_1:def 9 ;
then len (L_Cut f,p) = 2 by FINSEQ_1:61;
hence L_Cut f,p is unfolded by SPPOL_2:27; :: thesis: verum

end;

suppose p = f . ((Index p,f) + 1) ; :: thesis: L_Cut f,p is unfolded

then L_Cut f,p = mid f,(len f),(len f) by A23, A24, JORDAN3:def 4, NAT_1:13
.= <*(f /. (len f))*> by A6, JORDAN4:27 ;
then len (L_Cut f,p) = 1 by FINSEQ_1:56;
hence L_Cut f,p is unfolded by SPPOL_2:27; :: thesis: verum

end;

end;

end;

hence L_Cut f,p is unfolded ; :: thesis: verum

end;

end;