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;

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) ) )
;

end;

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;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

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;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

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))

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;.= (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

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))

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;

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;A40: now :: thesis: not p = (Rev f) . ((Index (p,(Rev f))) + 1)

A43:
Index (p,f) < len f
by A2, Th8;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;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

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