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:8;
A5: p in L~ (Rev f) by A2, SPPOL_2:22;
A6: Rev (Rev f) = f by FINSEQ_6:25;
A7: Rev f is s.n.c. by A1, SPPOL_2:35;
A8: dom (Rev f) = dom f by FINSEQ_5:57;
A9: len f = len (Rev f) by FINSEQ_5:def 3;
A10: 1 <= Index (p,f) by A2, JORDAN3:8;
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:8;
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:25;

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:235, XXREAL_0:2;
then A16: ((Rev f) /^ ((len (Rev f)) -' 1)) . 1 = (Rev f) . (len (Rev f)) by FINSEQ_6:114;
A17: len ((Rev f) /^ ((len (Rev f)) -' 1)) = (len (Rev f)) -' ((len (Rev f)) -' 1) by RFINSEQ:29;
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:233
.= 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:20
.= <*((Rev f) . (len (Rev f)))*> by A16, A19, FINSEQ_4:15 ;
A22: p = (Rev f) . (len f) by A14, FINSEQ_5:62;
then (Index (p,(Rev f))) + 1 = len f by A1, A7, A9, A11, Th18, SPPOL_2:28;
hence L_Cut ((Rev f),p) = <*p*> by A9, A22, A21, JORDAN3:def 3
.= Rev <*p*> by FINSEQ_5:60
.= Rev (R_Cut (f,p)) by A14, JORDAN3:def 4 ;
:: 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:58 ;
A28: (len f) -' (Index (p,f)) = (len f) - (Index (p,f)) by A4, XREAL_1:233
.= (Index (p,(Rev f))) + 1 by A26 ;
p <> (Rev f) . (len f) by A23, FINSEQ_5:62;
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 3
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(len f))) by A8, A13, A27, A28, A29, FINSEQ_6:126
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(((len f) -' 1) + 1))) by A10, A4, XREAL_1:235, XXREAL_0:2
.= <*p*> ^ (Rev (mid (f,1,(Index (p,f))))) by A10, A4, A11, FINSEQ_6:113
.= Rev ((mid (f,1,(Index (p,f)))) ^ <*p*>) by FINSEQ_5:63
.= Rev (R_Cut (f,p)) by A23, JORDAN3:def 4 ; :: 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:62;

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:28
.= ((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:58
.= f . ((Index (p,f)) + 1) by A9, A35 ;
hence contradiction by A31; :: thesis: verum

end;

A36: Index (p,f) < len f by A2, JORDAN3:8;
len f = (Index (p,(Rev f))) + (Index (p,f)) by A1, A2, A31, JORDAN3:21;
then Index (p,(Rev f)) = (len f) - (Index (p,f))
.= (len f) -' (Index (p,f)) by A36, XREAL_1:233 ;
hence L_Cut ((Rev f),p) = <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(len f))) by A9, A33, JORDAN3:def 3
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(((len f) -' 1) + 1))) by A10, A4, XREAL_1:235, XXREAL_0:2
.= <*p*> ^ (Rev (mid (f,1,(Index (p,f))))) by A10, A4, A11, FINSEQ_6:113
.= Rev ((mid (f,1,(Index (p,f)))) ^ <*p*>) by FINSEQ_5:63
.= Rev (R_Cut (f,p)) by A30, JORDAN3:def 4 ;
:: thesis: verum

end;

end;