let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) holds
L_Cut (Rev f),p = Rev (R_Cut f,p)
let p be Point of (TOP-REAL 2); :: thesis: ( f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) implies L_Cut (Rev f),p = Rev (R_Cut f,p) )
assume that
A1: ( f is poorly-one-to-one & f is unfolded & f is s.n.c. ) and
A2: p in L~ f and
A3: p <> f . (len f) ; :: thesis: L_Cut (Rev f),p = Rev (R_Cut f,p)
A4: Index p,f < len f by A2, JORDAN3:41;
A5: p in L~ (Rev f) by A2, SPPOL_2:22;
A6: Rev (Rev f) = f by FINSEQ_6:29;
A7: Rev f is s.n.c. by A1, SPPOL_2:36;
A8: dom (Rev f) = dom f by FINSEQ_5:60;
A9: len f = len (Rev f) by FINSEQ_5:def 3;
A10: 1 <= Index p,f by A2, JORDAN3:41;
then A11: 1 < len f by A4, XXREAL_0:2;
L~ f = L~ (Rev f) by SPPOL_2:22;
then Index p,(Rev f) < len (Rev f) by A2, JORDAN3:41;
then A12: (Index p,(Rev f)) + 1 <= len f by A9, NAT_1:13;
1 <= (Index p,(Rev f)) + 1 by NAT_1:11;
then A13: (Index p,(Rev f)) + 1 in dom f by A12, FINSEQ_3:27;

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

suppose A14: p = f . 1 ; :: thesis: L_Cut (Rev f),p = Rev (R_Cut f,p)

A15: ((len (Rev f)) -' 1) + 1 = len (Rev f) by A9, A10, A4, XREAL_1:237, XXREAL_0:2;
then A16: ((Rev f) /^ ((len (Rev f)) -' 1)) . 1 = (Rev f) . (len (Rev f)) by FINSEQ_6:120;
A17: len ((Rev f) /^ ((len (Rev f)) -' 1)) = (len (Rev f)) -' ((len (Rev f)) -' 1) by RFINSEQ:42;
A18: 1 <= (len (Rev f)) - ((len (Rev f)) -' 1) by A15;
then A19: 1 <= len ((Rev f) /^ ((len (Rev f)) -' 1)) by A17, NAT_D:39;
A20: not (Rev f) /^ ((len (Rev f)) -' 1) is empty by A17, A18, NAT_D:39;
((len (Rev f)) -' (len (Rev f))) + 1 = ((len (Rev f)) - (len (Rev f))) + 1 by XREAL_1:235
.= 1 ;
then A21: mid (Rev f),(len (Rev f)),(len (Rev f)) = ((Rev f) /^ ((len (Rev f)) -' 1)) | 1 by FINSEQ_6:def 3
.= <*(((Rev f) /^ ((len (Rev f)) -' 1)) /. 1)*> by A20, FINSEQ_5:23
.= <*((Rev f) . (len (Rev f)))*> by A16, A19, FINSEQ_4:24 ;
A22: p = (Rev f) . (len f) by A14, FINSEQ_5:65;
then (Index p,(Rev f)) + 1 = len f by A1, A7, A9, A11, Th18, SPPOL_2:29;
hence L_Cut (Rev f),p = <*p*> by A9, A22, A21, JORDAN3:def 4
.= Rev <*p*> by FINSEQ_5:63
.= Rev (R_Cut f,p) by A14, JORDAN3:def 5 ;
:: thesis: verum

end;

suppose that A23: p <> f . 1 and
A24: p <> f . (len f) and
A25: p = f . ((Index p,f) + 1) ; :: thesis: L_Cut (Rev f),p = Rev (R_Cut f,p)

A26: len f = ((Index p,(Rev f)) + (Index p,f)) + 1 by A1, A2, A24, A25, Th36
.= (Index p,f) + ((Index p,(Rev f)) + 1) ;
len f = ((Index p,(Rev f)) + (Index p,f)) + 1 by A1, A2, A24, A25, Th36
.= (Index p,(Rev f)) + ((Index p,f) + 1) ;
then A27: p = f . (((len f) - ((Index p,(Rev f)) + 1)) + 1) by A25
.= (Rev f) . ((Index p,(Rev f)) + 1) by A13, FINSEQ_5:61 ;
A28: (len f) -' (Index p,f) = (len f) - (Index p,f) by A4, XREAL_1:235
.= (Index p,(Rev f)) + 1 by A26 ;
p <> (Rev f) . (len f) by A23, FINSEQ_5:65;
then A29: (Index p,(Rev f)) + 1 < len f by A12, A27, XXREAL_0:1;
thus L_Cut (Rev f),p = mid (Rev f),((Index p,(Rev f)) + 1),(len f) by A9, A27, JORDAN3:def 4
.= <*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(len f)) by A8, A13, A27, A28, A29, FINSEQ_6:132
.= <*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(((len f) -' 1) + 1)) by A10, A4, XREAL_1:237, XXREAL_0:2
.= <*p*> ^ (Rev (mid f,1,(Index p,f))) by A10, A4, A11, FINSEQ_6:119
.= Rev ((mid f,1,(Index p,f)) ^ <*p*>) by FINSEQ_5:66
.= Rev (R_Cut f,p) by A23, JORDAN3:def 5 ; :: thesis: verum

end;

suppose that A30: p <> f . 1 and
A31: p <> f . ((Index p,f) + 1) ; :: thesis: L_Cut (Rev f),p = Rev (R_Cut f,p)

A32: p <> (Rev f) . (len f) by A30, FINSEQ_5:65;

A33: now

assume A34: p = (Rev f) . ((Index p,(Rev f)) + 1) ; :: thesis: contradiction
then A35: len (Rev f) = ((Index p,(Rev (Rev f))) + (Index p,(Rev f))) + 1 by A1, A7, A5, A9, A32, Th36, SPPOL_2:29
.= ((Index p,f) + 1) + (Index p,(Rev f)) by A6 ;
p = f . (((len f) - ((Index p,(Rev f)) + 1)) + 1) by A13, A34, FINSEQ_5:61
.= f . ((Index p,f) + 1) by A9, A35 ;
hence contradiction by A31; :: thesis: verum

end;

A36: Index p,f < len f by A2, JORDAN3:41;
len f = (Index p,(Rev f)) + (Index p,f) by A1, A2, A31, JORDAN3:54;
then Index p,(Rev f) = (len f) - (Index p,f)
.= (len f) -' (Index p,f) by A36, XREAL_1:235 ;
hence L_Cut (Rev f),p = <*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(len f)) by A9, A33, JORDAN3:def 4
.= <*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(((len f) -' 1) + 1)) by A10, A4, XREAL_1:237, XXREAL_0:2
.= <*p*> ^ (Rev (mid f,1,(Index p,f))) by A10, A4, A11, FINSEQ_6:119
.= Rev ((mid f,1,(Index p,f)) ^ <*p*>) by FINSEQ_5:66
.= Rev (R_Cut f,p) by A30, JORDAN3:def 5 ;
:: thesis: verum

end;

end;