let f be FinSequence of (); :: thesis: for p being Point of () 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 (); :: 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 ;
A5: 1 <= Index (p,f) by ;
A6: Rev f is being_S-Seq by A1;
A7: Rev (Rev f) = f ;
A8: Index (p,f) < len f by ;
L~ f = L~ (Rev f) by SPPOL_2:22;
then Index (p,(Rev f)) < len (Rev f) by ;
then A9: (Index (p,(Rev f))) + 1 <= len f by ;
1 <= (Index (p,(Rev f))) + 1 by NAT_1:11;
then A10: (Index (p,(Rev f))) + 1 in dom f by ;
A11: 1 + 1 <= len f by ;
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 ;
A15: 2 in dom f by ;
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 ;
A19: p = (Rev f) . 1 by ;
then A20: p <> (Rev f) . (1 + 1) by ;
p = (Rev f) /. 1 by ;
then A21: Index (p,(Rev f)) = 1 by ;
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
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(((len f) -' 1) + 1))) by
.= <*p*> ^ (Rev (mid (f,1,(Index (p,f))))) by
.= Rev ((mid (f,1,(Index (p,f)))) ^ <*p*>) by FINSEQ_5:63
.= Rev (R_Cut (f,p)) by ; :: 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 ;
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 ;
((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
.= <*((Rev f) . (len (Rev f)))*> by A25 ;
A29: p = (Rev f) . (len f) by ;
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 ;
:: 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 ;
A35: (len f) -' (Index (p,f)) = (len f) - (Index (p,f)) by
.= (Index (p,(Rev f))) + 1 by A33 ;
p <> (Rev f) . (len f) by ;
then A36: (Index (p,(Rev f))) + 1 < len f by ;
thus L_Cut ((Rev f),p) = mid ((Rev f),((Index (p,(Rev f))) + 1),(len f)) by
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(len f))) by
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(((len f) -' 1) + 1))) by
.= <*p*> ^ (Rev (mid (f,1,(Index (p,f))))) by
.= Rev ((mid (f,1,(Index (p,f)))) ^ <*p*>) by FINSEQ_5:63
.= Rev (R_Cut (f,p)) by ; :: 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 ;
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
.= f . ((Index (p,f)) + 1) by ;
hence contradiction by A38; :: thesis: verum
end;
A43: Index (p,f) < len f by ;
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 ;
hence L_Cut ((Rev f),p) = <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(len f))) by
.= <*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(((len f) -' 1) + 1))) by
.= <*p*> ^ (Rev (mid (f,1,(Index (p,f))))) by
.= Rev ((mid (f,1,(Index (p,f)))) ^ <*p*>) by FINSEQ_5:63
.= Rev (R_Cut (f,p)) by ;
:: thesis: verum
end;
end;