let f be FinSequence of (TOP-REAL 2); 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); ( 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
; 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)
;
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
;
verum end; suppose A23:
p = f . 1
;
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
;
verum end; suppose that A30:
p <> f . 1
and A31:
p <> f . (len f)
and A32:
p = f . ((Index (p,f)) + 1)
;
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
;
verum end; suppose that A37:
p <> f . 1
and A38:
p <> f . ((Index (p,f)) + 1)
;
L_Cut ((Rev f),p) = Rev (R_Cut (f,p))A39:
p <> (Rev f) . (len f)
by A37, FINSEQ_5:62;
A40:
now not p = (Rev f) . ((Index (p,(Rev f))) + 1)assume A41:
p = (Rev f) . ((Index (p,(Rev f))) + 1)
;
contradictionthen 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;
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
;
verum end;