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
R_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
R_Cut (f,p) is unfolded
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies R_Cut (f,p) is unfolded )
assume A2: p in L~ f ; :: thesis: R_Cut (f,p) is unfolded
then A3: 1 <= Index (p,f) by JORDAN3:8;
len f <> 0 by A2, TOPREAL1:22;
then len f > 0 by NAT_1:3;
then A4: len f >= 0 + 1 by NAT_1:13;
then 1 in Seg (len f) by FINSEQ_1:1;
then A5: 1 in dom f by FINSEQ_1:def 3;
A6: Index (p,f) < len f by A2, JORDAN3:8;
then A7: ((Index (p,f)) + 1) + 0 <= len f by NAT_1:13;
then A8: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, TOPREAL1:def 3;
Index (p,f) in Seg (len f) by A3, A6, FINSEQ_1:1;
then A9: Index (p,f) in dom f by FINSEQ_1:def 3;
then A10: (mid (f,1,(Index (p,f)))) /. (len (mid (f,1,(Index (p,f))))) = f /. (Index (p,f)) by A5, SPRECT_2:9;
A11: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, JORDAN5B:29;
A12: ((Index (p,f)) -' 1) + 1 = Index (p,f) by A2, JORDAN3:8, XREAL_1:235;

per cases ( Index (p,f) > 0 + 1 or Index (p,f) = 0 + 1 ) by A3, XXREAL_0:1;

suppose A13: Index (p,f) > 0 + 1 ; :: thesis: R_Cut (f,p) is unfolded

A14: f /. (Index (p,f)) in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by RLTOPSP1:68;
A15: f /. (Index (p,f)) in LSeg ((f /. (Index (p,f))),p) by RLTOPSP1:68;
f /. (Index (p,f)) in LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f)))) by RLTOPSP1:68;
then f /. (Index (p,f)) in (LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f))))) /\ (LSeg ((f /. (Index (p,f))),p)) by A15, XBOOLE_0:def 4;
then A16: {(f /. (Index (p,f)))} c= (LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f))))) /\ (LSeg ((f /. (Index (p,f))),p)) by ZFMISC_1:31;
A17: ((Index (p,f)) -' 1) + (1 + 1) <= len f by A7, A12;
(Index (p,f)) - 1 > 0 by A13, XREAL_1:20;
then (Index (p,f)) -' 1 > 0 by XREAL_0:def 2;
then A18: (Index (p,f)) -' 1 >= 0 + 1 by NAT_1:13;
then LSeg (f,((Index (p,f)) -' 1)) = LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f)))) by A6, A12, TOPREAL1:def 3;
then (LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f))))) /\ (LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1)))) = {(f /. (Index (p,f)))} by A1, A12, A8, A18, A17, TOPREAL1:def 6;
then (LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f))))) /\ (LSeg ((f /. (Index (p,f))),p)) c= {(f /. (Index (p,f)))} by A11, A14, TOPREAL1:6, XBOOLE_1:26;
then A19: (LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f))))) /\ (LSeg ((f /. (Index (p,f))),p)) = {(f /. (Index (p,f)))} by A16;
A20: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by A4, A3, A6, FINSEQ_6:118
.= Index (p,f) by A2, JORDAN3:8, XREAL_1:235 ;
then A21: ((len (mid (f,1,(Index (p,f))))) -' 1) + 1 = len (mid (f,1,(Index (p,f)))) by A2, JORDAN3:8, XREAL_1:235;
(len (mid (f,1,(Index (p,f))))) -' 1 <= len (mid (f,1,(Index (p,f)))) by NAT_D:35;
then (len (mid (f,1,(Index (p,f))))) -' 1 in Seg (len (mid (f,1,(Index (p,f))))) by A18, A20, FINSEQ_1:1;
then (len (mid (f,1,(Index (p,f))))) -' 1 in dom (mid (f,1,(Index (p,f)))) by FINSEQ_1:def 3;
then A22: (mid (f,1,(Index (p,f)))) /. ((len (mid (f,1,(Index (p,f))))) -' 1) = f /. ((((len (mid (f,1,(Index (p,f))))) -' 1) + 1) -' 1) by A2, A9, A5, JORDAN3:8, SPRECT_2:3
.= f /. ((len (mid (f,1,(Index (p,f))))) -' 1) by NAT_D:34
.= f /. ((((Index (p,f)) -' 1) + 1) -' 1) by A3, A6, FINSEQ_6:186
.= f /. ((Index (p,f)) -' 1) by A2, JORDAN3:8, XREAL_1:235 ;
((len (mid (f,1,(Index (p,f))))) -' 1) + 1 = len (mid (f,1,(Index (p,f)))) by A2, A20, JORDAN3:8, XREAL_1:235;
then A23: LSeg ((mid (f,1,(Index (p,f)))),((len (mid (f,1,(Index (p,f))))) -' 1)) = LSeg ((f /. ((Index (p,f)) -' 1)),(f /. (Index (p,f)))) by A10, A18, A20, A22, TOPREAL1:def 3;

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

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

suppose p <> f . 1 ; :: thesis: R_Cut (f,p) is unfolded

then R_Cut (f,p) = (mid (f,1,(Index (p,f)))) ^ <*p*> by JORDAN3:def 4;
hence R_Cut (f,p) is unfolded by A1, A10, A23, A21, A19, Th28, SPPOL_2:30; :: thesis: verum

end;

suppose p = f . 1 ; :: thesis: R_Cut (f,p) is unfolded

then R_Cut (f,p) = <*p*> by JORDAN3:def 4;
then len (R_Cut (f,p)) = 1 by FINSEQ_1:39;
hence R_Cut (f,p) is unfolded by SPPOL_2:26; :: thesis: verum

end;

end;

end;

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

end;

suppose A24: Index (p,f) = 0 + 1 ; :: thesis: R_Cut (f,p) is unfolded

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

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

suppose p <> f . 1 ; :: thesis: R_Cut (f,p) is unfolded

then R_Cut (f,p) = (mid (f,1,1)) ^ <*p*> by A24, JORDAN3:def 4
.= <*(f . 1)*> ^ <*p*> by A5, FINSEQ_6:193
.= <*(f /. 1)*> ^ <*p*> by A5, PARTFUN1:def 6
.= <*(f /. 1),p*> by FINSEQ_1:def 9 ;
then len (R_Cut (f,p)) = 2 by FINSEQ_1:44;
hence R_Cut (f,p) is unfolded by SPPOL_2:26; :: thesis: verum

end;

suppose p = f . 1 ; :: thesis: R_Cut (f,p) is unfolded

then R_Cut (f,p) = <*p*> by JORDAN3:def 4;
then len (R_Cut (f,p)) = 1 by FINSEQ_1:39;
hence R_Cut (f,p) is unfolded by SPPOL_2:26; :: thesis: verum

end;

end;

end;

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

end;

end;