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 f is s.n.c. by A1, SPPOL_2:35;
A7: dom (Rev f) = dom f by FINSEQ_5:57;
A8: len f = len (Rev f) by FINSEQ_5:def 3;
A9: 1 <= Index (p,f) by A2, JORDAN3:8;
then A10: 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 A11: (Index (p,(Rev f))) + 1 <= len f by A8, NAT_1:13;
1 <= (Index (p,(Rev f))) + 1 by NAT_1:11;
then A12: (Index (p,(Rev f))) + 1 in dom f by A11, 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 A13: p = f . 1 ; :: thesis: L_Cut ((Rev f),p) = Rev (R_Cut (f,p))

A14: ((len (Rev f)) -' 1) + 1 = len (Rev f) by A8, A9, A4, XREAL_1:235, XXREAL_0:2;
then A15: ((Rev f) /^ ((len (Rev f)) -' 1)) . 1 = (Rev f) . (len (Rev f)) by FINSEQ_6:114;
A16: len ((Rev f) /^ ((len (Rev f)) -' 1)) = (len (Rev f)) -' ((len (Rev f)) -' 1) by RFINSEQ:29;
A17: 1 <= (len (Rev f)) - ((len (Rev f)) -' 1) by A14;
A19: not (Rev f) /^ ((len (Rev f)) -' 1) is empty by A16, A17, NAT_D:39;
((len (Rev f)) -' (len (Rev f))) + 1 = ((len (Rev f)) - (len (Rev f))) + 1 by XREAL_1:233
.= 1 ;
then A20: 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 A19, FINSEQ_5:20
.= <*((Rev f) . (len (Rev f)))*> by A15 ;
A21: p = (Rev f) . (len f) by A13, FINSEQ_5:62;
then (Index (p,(Rev f))) + 1 = len f by A1, A6, A8, A10, Th18, SPPOL_2:28;
hence L_Cut ((Rev f),p) = <*p*> by A8, A21, A20, JORDAN3:def 3
.= Rev <*p*> by FINSEQ_5:60
.= Rev (R_Cut (f,p)) by A13, JORDAN3:def 4 ;
:: thesis: verum

end;

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

A25: len f = ((Index (p,(Rev f))) + (Index (p,f))) + 1 by A1, A2, A23, A24, Th36
.= (Index (p,f)) + ((Index (p,(Rev f))) + 1) ;
len f = ((Index (p,(Rev f))) + (Index (p,f))) + 1 by A1, A2, A23, A24, Th36
.= (Index (p,(Rev f))) + ((Index (p,f)) + 1) ;
then A26: p = f . (((len f) - ((Index (p,(Rev f))) + 1)) + 1) by A24
.= (Rev f) . ((Index (p,(Rev f))) + 1) by A12, FINSEQ_5:58 ;
A27: (len f) -' (Index (p,f)) = (len f) - (Index (p,f)) by A4, XREAL_1:233
.= (Index (p,(Rev f))) + 1 by A25 ;
p <> (Rev f) . (len f) by A22, FINSEQ_5:62;
then A28: (Index (p,(Rev f))) + 1 < len f by A11, A26, XXREAL_0:1;
thus L_Cut ((Rev f),p) = mid ((Rev f),((Index (p,(Rev f))) + 1),(len f)) by A8, A26, JORDAN3:def 3
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(len f))) by A7, A12, A26, A27, A28, FINSEQ_6:126
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(((len f) -' 1) + 1))) by A9, A4, XREAL_1:235, XXREAL_0:2
.= <*p*> ^ (Rev (mid (f,1,(Index (p,f))))) by A9, A4, A10, FINSEQ_6:113
.= Rev ((mid (f,1,(Index (p,f)))) ^ <*p*>) by FINSEQ_5:63
.= Rev (R_Cut (f,p)) by A22, JORDAN3:def 4 ; :: thesis: verum

end;

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

A31: p <> (Rev f) . (len f) by A29, FINSEQ_5:62;

A32: now :: thesis: not p = (Rev f) . ((Index (p,(Rev f))) + 1)

assume A33: p = (Rev f) . ((Index (p,(Rev f))) + 1) ; :: thesis: contradiction
then A34: len (Rev f) = ((Index (p,(Rev (Rev f)))) + (Index (p,(Rev f)))) + 1 by A1, A6, A5, A8, A31, Th36, SPPOL_2:28
.= ((Index (p,f)) + 1) + (Index (p,(Rev f))) ;
p = f . (((len f) - ((Index (p,(Rev f))) + 1)) + 1) by A12, A33, FINSEQ_5:58
.= f . ((Index (p,f)) + 1) by A8, A34 ;
hence contradiction by A30; :: thesis: verum

end;

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

end;

end;