let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f holds
L_Cut ((Rev f),p) = Rev (R_Cut (f,p))
let p be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p in L~ f implies L_Cut ((Rev f),p) = Rev (R_Cut (f,p)) )
assume that
A1: f is being_S-Seq and
A2: p in L~ f ; :: thesis: L_Cut ((Rev f),p) = Rev (R_Cut (f,p))
A3: len f = len (Rev f) by FINSEQ_5:def 3;
A4: p in L~ (Rev f) by A2, SPPOL_2:22;
A5: 1 <= Index (p,f) by A2, Th8;
A6: Rev f is being_S-Seq by A1;
A7: Rev (Rev f) = f ;
A8: Index (p,f) < len f by A2, Th8;
L~ f = L~ (Rev f) by SPPOL_2:22;
then Index (p,(Rev f)) < len (Rev f) by A2, Th8;
then A9: (Index (p,(Rev f))) + 1 <= len f by A3, NAT_1:13;
1 <= (Index (p,(Rev f))) + 1 by NAT_1:11;
then A10: (Index (p,(Rev f))) + 1 in dom f by A9, FINSEQ_3:25;
A11: 1 + 1 <= len f by A1, TOPREAL1:def 8;
then A12: 1 < len f by NAT_1:13;
then A13: 1 in dom f by FINSEQ_3:25;
A14: len f in dom f by A12, FINSEQ_3:25;
A15: 2 in dom f by A11, FINSEQ_3:25;
A16: dom (Rev f) = dom f by FINSEQ_5:57;

per cases ( p = f . (len f) or 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) ) ) ;

suppose A17: p = f . (len f) ; :: thesis: L_Cut ((Rev f),p) = Rev (R_Cut (f,p))

then A18: p <> f . 1 by A1, A12, A13, A14, FUNCT_1:def 4;
A19: p = (Rev f) . 1 by A17, FINSEQ_5:62;
then A20: p <> (Rev f) . (1 + 1) by A1, A16, A13, A15, FUNCT_1:def 4;
p = (Rev f) /. 1 by A16, A13, A19, PARTFUN1:def 6;
then A21: Index (p,(Rev f)) = 1 by A3, A11, Th11;
then (Index (p,(Rev f))) + (Index (p,f)) = len f by A6, A4, A7, A3, A20, Th21;
then A22: Index (p,(Rev f)) = (len f) - (Index (p,f)) ;
thus L_Cut ((Rev f),p) = <*p*> ^ (mid ((Rev f),((Index (p,(Rev f))) + 1),(len f))) by A3, A21, A20, Def3
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(len f))) by A8, A22, XREAL_1:233
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(((len f) -' 1) + 1))) by A12, XREAL_1:235
.= <*p*> ^ (Rev (mid (f,1,(Index (p,f))))) by A12, A5, A8, FINSEQ_6:113
.= Rev ((mid (f,1,(Index (p,f)))) ^ <*p*>) by FINSEQ_5:63
.= Rev (R_Cut (f,p)) by A18, Def4 ; :: thesis: verum

end;

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

A24: ((len (Rev f)) -' 1) + 1 = len (Rev f) by A3, A12, XREAL_1:235;
then A25: ((Rev f) /^ ((len (Rev f)) -' 1)) . 1 = (Rev f) . (len (Rev f)) by FINSEQ_6:114;
A26: len ((Rev f) /^ ((len (Rev f)) -' 1)) = (len (Rev f)) -' ((len (Rev f)) -' 1) by RFINSEQ:29;
1 <= (len (Rev f)) - ((len (Rev f)) -' 1) by A24;
then A27: 1 <= len ((Rev f) /^ ((len (Rev f)) -' 1)) by A26, NAT_D:39;
((len (Rev f)) -' (len (Rev f))) + 1 = ((len (Rev f)) - (len (Rev f))) + 1 by XREAL_1:233
.= 1 ;
then A28: 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 A27, CARD_1:27, FINSEQ_5:20
.= <*((Rev f) . (len (Rev f)))*> by A25 ;
A29: p = (Rev f) . (len f) by A23, FINSEQ_5:62;
then (Index (p,(Rev f))) + 1 = len f by A1, A3, A12, Th12;
hence L_Cut ((Rev f),p) = <*p*> by A3, A29, A28, Def3
.= Rev <*p*> by FINSEQ_5:60
.= Rev (R_Cut (f,p)) by A23, Def4 ;
:: thesis: verum

end;

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

A33: len f = ((Index (p,(Rev f))) + (Index (p,f))) + 1 by A1, A2, A31, A32, Th20
.= (Index (p,f)) + ((Index (p,(Rev f))) + 1) ;
len f = ((Index (p,(Rev f))) + (Index (p,f))) + 1 by A1, A2, A31, A32, Th20
.= (Index (p,(Rev f))) + ((Index (p,f)) + 1) ;
then A34: p = f . (((len f) - ((Index (p,(Rev f))) + 1)) + 1) by A32
.= (Rev f) . ((Index (p,(Rev f))) + 1) by A10, FINSEQ_5:58 ;
A35: (len f) -' (Index (p,f)) = (len f) - (Index (p,f)) by A8, XREAL_1:233
.= (Index (p,(Rev f))) + 1 by A33 ;
p <> (Rev f) . (len f) by A30, FINSEQ_5:62;
then A36: (Index (p,(Rev f))) + 1 < len f by A9, A34, XXREAL_0:1;
thus L_Cut ((Rev f),p) = mid ((Rev f),((Index (p,(Rev f))) + 1),(len f)) by A3, A34, Def3
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(len f))) by A16, A10, A34, A35, A36, FINSEQ_6:126
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(((len f) -' 1) + 1))) by A12, XREAL_1:235
.= <*p*> ^ (Rev (mid (f,1,(Index (p,f))))) by A12, A5, A8, FINSEQ_6:113
.= Rev ((mid (f,1,(Index (p,f)))) ^ <*p*>) by FINSEQ_5:63
.= Rev (R_Cut (f,p)) by A30, Def4 ; :: thesis: verum

end;

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

A39: p <> (Rev f) . (len f) by A37, FINSEQ_5:62;

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

assume A41: p = (Rev f) . ((Index (p,(Rev f))) + 1) ; :: thesis: contradiction
then A42: len (Rev f) = ((Index (p,(Rev (Rev f)))) + (Index (p,(Rev f)))) + 1 by A1, A4, A3, A39, Th20
.= ((Index (p,f)) + 1) + (Index (p,(Rev f))) ;
p = f . (((len f) - ((Index (p,(Rev f))) + 1)) + 1) by A10, A41, FINSEQ_5:58
.= f . ((Index (p,f)) + 1) by A3, A42 ;
hence contradiction by A38; :: thesis: verum

end;

A43: Index (p,f) < len f by A2, Th8;
len f = (Index (p,(Rev f))) + (Index (p,f)) by A1, A2, A38, Th21;
then Index (p,(Rev f)) = (len f) - (Index (p,f))
.= (len f) -' (Index (p,f)) by A43, XREAL_1:233 ;
hence L_Cut ((Rev f),p) = <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(len f))) by A3, A40, Def3
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(((len f) -' 1) + 1))) by A12, XREAL_1:235
.= <*p*> ^ (Rev (mid (f,1,(Index (p,f))))) by A12, A5, A8, FINSEQ_6:113
.= Rev ((mid (f,1,(Index (p,f)))) ^ <*p*>) by FINSEQ_5:63
.= Rev (R_Cut (f,p)) by A37, Def4 ;
:: thesis: verum

end;

end;