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:41;
len f <> 0 by A2, TOPREAL1:28;
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:3;
then A5: 1 in dom f by FINSEQ_1:def 3;
A6: Index p,f < len f by A2, JORDAN3:41;
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 5;
Index p,f in Seg (len f) by A3, A6, FINSEQ_1:3;
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:13;
A11: p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A2, JORDAN5B:32;
A12: ((Index p,f) -' 1) + 1 = Index p,f by A2, JORDAN3:41, XREAL_1:237;

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:69;
A15: f /. (Index p,f) in LSeg (f /. (Index p,f)),p by RLTOPSP1:69;
f /. (Index p,f) in LSeg (f /. ((Index p,f) -' 1)),(f /. (Index p,f)) by RLTOPSP1:69;
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:37;
A17: ((Index p,f) -' 1) + (1 + 1) <= len f by A7, A12;
(Index p,f) - 1 > 0 by A13, XREAL_1:22;
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 5;
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 8;
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:12, 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, XBOOLE_0:def 10;
A20: len (mid f,1,(Index p,f)) = ((Index p,f) -' 1) + 1 by A4, A3, A6, JORDAN3:27
.= Index p,f by A2, JORDAN3:41, XREAL_1:237 ;
then A21: ((len (mid f,1,(Index p,f))) -' 1) + 1 = len (mid f,1,(Index p,f)) by A2, JORDAN3:41, XREAL_1:237;
(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:3;
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:41, SPRECT_2:7
.= f /. ((len (mid f,1,(Index p,f))) -' 1) by NAT_D:34
.= f /. ((((Index p,f) -' 1) + 1) -' 1) by A3, A6, JORDAN4:20
.= f /. ((Index p,f) -' 1) by A2, JORDAN3:41, XREAL_1:237 ;
((len (mid f,1,(Index p,f))) -' 1) + 1 = len (mid f,1,(Index p,f)) by A2, A20, JORDAN3:41, XREAL_1:237;
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 5;

now

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 5;
hence R_Cut f,p is unfolded by A1, A10, A23, A21, A19, Th28, SPPOL_2:31; :: thesis: verum

end;

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

then R_Cut f,p = <*p*> by JORDAN3:def 5;
then len (R_Cut f,p) = 1 by FINSEQ_1:56;
hence R_Cut f,p is unfolded by SPPOL_2:27; :: 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

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 5
.= <*(f /. 1)*> ^ <*p*> by A4, JORDAN4:27
.= <*(f /. 1),p*> by FINSEQ_1:def 9 ;
then len (R_Cut f,p) = 2 by FINSEQ_1:61;
hence R_Cut f,p is unfolded by SPPOL_2:27; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

end;