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:29;
Index (p,f) < len f by A3, JORDAN3:8;
then A5: ((Index (p,f)) + 1) + 0 <= len f by NAT_1:13;
len f <> 0 by A3, TOPREAL1:22;
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:25;
A8: 1 <= Index (p,f) by A3, JORDAN3:8;
then A9: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A5, TOPREAL1:def 3;
A10: 1 < (Index (p,f)) + 1 by A8, NAT_1:13;
then A11: (Index (p,f)) + 1 in dom f by A5, FINSEQ_3:25;
then A12: (mid (f,((Index (p,f)) + 1),(len f))) /. 1 = f /. ((Index (p,f)) + 1) by A7, SPRECT_2:8;

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 3;
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 6;
A15: (len f) - ((Index (p,f)) + 1) >= 0 by A5, XREAL_1:19;
(Index (p,f)) + (1 + 1) <= len f by A13;
then A16: 2 <= (len f) - (Index (p,f)) by XREAL_1:19;
A17: f /. ((Index (p,f)) + 1) in LSeg ((f /. ((Index (p,f)) + 1)),(f /. ((Index (p,f)) + (1 + 1)))) by RLTOPSP1:68;
f /. ((Index (p,f)) + 1) in LSeg (p,(f /. ((Index (p,f)) + 1))) by RLTOPSP1:68;
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:31;
(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:118
.= ((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:25;
then (mid (f,((Index (p,f)) + 1),(len f))) /. 2 = f /. ((2 + ((Index (p,f)) + 1)) -' 1) by A5, A11, A7, SPRECT_2:3
.= 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 3;
f /. ((Index (p,f)) + 1) in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by RLTOPSP1:68;
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:6, 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;

now :: thesis: L_Cut (f,p) is unfolded

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 3;
hence L_Cut (f,p) is unfolded by A1, A12, A21, A22, Th28, SPPOL_2:29; :: 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 3; :: 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 :: thesis: L_Cut (f,p) is unfolded

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 3, NAT_1:13
.= <*p*> ^ <*(f . (len f))*> by A7, FINSEQ_6:193
.= <*p*> ^ <*(f /. (len f))*> by A7, PARTFUN1:def 6
.= <*p,(f /. (len f))*> by FINSEQ_1:def 9 ;
then len (L_Cut (f,p)) = 2 by FINSEQ_1:44;
hence L_Cut (f,p) is unfolded by SPPOL_2:26; :: 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 3, NAT_1:13
.= <*(f . (len f))*> by A7, FINSEQ_6:193 ;
then len (L_Cut (f,p)) = 1 by FINSEQ_1:39;
hence L_Cut (f,p) is unfolded by SPPOL_2:26; :: thesis: verum

end;

end;

end;

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

end;

end;