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 )
assume A2: p in L~ f ; :: thesis: L_Cut f,p is unfolded
then len f <> 0 by TOPREAL1:28;
then len f > 0 by NAT_1:3;
then A3: len f >= 0 + 1 by NAT_1:13;
A4: mid f,((Index p,f) + 1),(len f) is unfolded by A1, Th28;
A5: ( 1 <= Index p,f & Index p,f < len f ) by A2, JORDAN3:41;
then A6: ( 1 < (Index p,f) + 1 & ((Index p,f) + 1) + 0 <= len f ) by NAT_1:13;
then A7: ( (Index p,f) + 1 in dom f & len f in dom f ) by A3, FINSEQ_3:27;
then A8: (mid f,((Index p,f) + 1),(len f)) /. 1 = f /. ((Index p,f) + 1) by SPRECT_2:12;
A9: p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A2, JORDAN5B:32;
A10: LSeg f,(Index p,f) = LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A5, A6, TOPREAL1:def 5;

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

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

then A12: LSeg f,((Index p,f) + 1) = LSeg (f /. ((Index p,f) + 1)),(f /. ((Index p,f) + (1 + 1))) by A6, TOPREAL1:def 5;
A13: (len f) - ((Index p,f) + 1) >= 0 by A6, XREAL_1:21;
(2 + ((Index p,f) + 1)) - 1 = ((Index p,f) + 1) + 1 ;
then A14: (2 + ((Index p,f) + 1)) - 1 >= 0 by NAT_1:2;
A15: len (mid f,((Index p,f) + 1),(len f)) = ((len f) -' ((Index p,f) + 1)) + 1 by A3, A6, JORDAN3:27
.= ((len f) - ((Index p,f) + 1)) + 1 by A13, XREAL_0:def 2
.= (len f) - (Index p,f) ;
(Index p,f) + (1 + 1) <= len f by A11;
then A16: 2 <= (len f) - (Index p,f) by XREAL_1:21;
then 2 in dom (mid f,((Index p,f) + 1),(len f)) by A15, FINSEQ_3:27;
then (mid f,((Index p,f) + 1),(len f)) /. 2 = f /. ((2 + ((Index p,f) + 1)) -' 1) by A6, A7, SPRECT_2:7
.= f /. ((Index p,f) + (1 + 1)) by A14, XREAL_0:def 2 ;
then A17: LSeg (mid f,((Index p,f) + 1),(len f)),1 = LSeg (f /. ((Index p,f) + 1)),(f /. ((Index p,f) + (1 + 1))) by A8, A15, A16, TOPREAL1:def 5;
A18: (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, A5, A10, A11, A12, TOPREAL1:def 8;
f /. ((Index p,f) + 1) in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by RLTOPSP1:69;
then A19: (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 A9, A18, TOPREAL1:12, XBOOLE_1:26;
( f /. ((Index p,f) + 1) in LSeg p,(f /. ((Index p,f) + 1)) & f /. ((Index p,f) + 1) in LSeg (f /. ((Index p,f) + 1)),(f /. ((Index p,f) + (1 + 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 XBOOLE_0:def 4;
then {(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;
then A20: (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 A19, 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, A8, A17, A20, 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 A4, JORDAN3:def 4; :: thesis: verum

end;

end;

end;

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

end;

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

A22: ( (Index p,f) + 1 < len f or (Index p,f) + 1 = len f ) by A6, 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 A21, A22, JORDAN3:def 4, NAT_1:13
.= <*p*> ^ <*(f /. (len f))*> by A3, 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 A21, A22, JORDAN3:def 4, NAT_1:13
.= <*(f /. (len f))*> by A3, 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;