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, Th41;
A6:
Rev f is being_S-Seq
by A1;
A7:
Rev (Rev f) = f
by FINSEQ_6:29;
A8:
Index p,f < len f
by A2, Th41;
L~ f = L~ (Rev f)
by SPPOL_2:22;
then
Index p,(Rev f) < len (Rev f)
by A2, Th41;
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:27;
A11:
1 + 1 <= len f
by A1, TOPREAL1:def 10;
then A12:
1 < len f
by NAT_1:13;
then A13:
1 in dom f
by FINSEQ_3:27;
A14:
len f in dom f
by A12, FINSEQ_3:27;
A15:
2 in dom f
by A11, FINSEQ_3:27;
A16:
dom (Rev f) = dom f
by FINSEQ_5:60;
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 8;
A19:
p = (Rev f) . 1
by A17, FINSEQ_5:65;
then A20:
p <> (Rev f) . (1 + 1)
by A1, A16, A13, A15, FUNCT_1:def 8;
p = (Rev f) /. 1
by A16, A13, A19, PARTFUN1:def 8;
then A21:
Index p,
(Rev f) = 1
by A3, A11, Th44;
then
(Index p,(Rev f)) + (Index p,f) = len f
by A6, A4, A7, A3, A20, Th54;
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, Def4
.=
<*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(len f))
by A8, A22, XREAL_1:235
.=
<*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(((len f) -' 1) + 1))
by A12, XREAL_1:237
.=
<*p*> ^ (Rev (mid f,1,(Index p,f)))
by A12, A5, A8, FINSEQ_6:119
.=
Rev ((mid f,1,(Index p,f)) ^ <*p*>)
by FINSEQ_5:66
.=
Rev (R_Cut f,p)
by A18, Def5
;
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:237;
then A25:
((Rev f) /^ ((len (Rev f)) -' 1)) . 1
= (Rev f) . (len (Rev f))
by FINSEQ_6:120;
A26:
len ((Rev f) /^ ((len (Rev f)) -' 1)) = (len (Rev f)) -' ((len (Rev f)) -' 1)
by RFINSEQ:42;
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:235
.=
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:47, FINSEQ_5:23
.=
<*((Rev f) . (len (Rev f)))*>
by A25, A27, FINSEQ_4:24
;
A29:
p = (Rev f) . (len f)
by A23, FINSEQ_5:65;
then
(Index p,(Rev f)) + 1
= len f
by A1, A3, A12, Th45;
hence L_Cut (Rev f),
p =
<*p*>
by A3, A29, A28, Def4
.=
Rev <*p*>
by FINSEQ_5:63
.=
Rev (R_Cut f,p)
by A23, Def5
;
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, Th53
.=
(Index p,f) + ((Index p,(Rev f)) + 1)
;
len f =
((Index p,(Rev f)) + (Index p,f)) + 1
by A1, A2, A31, A32, Th53
.=
(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:61
;
A35:
(len f) -' (Index p,f) =
(len f) - (Index p,f)
by A8, XREAL_1:235
.=
(Index p,(Rev f)) + 1
by A33
;
p <> (Rev f) . (len f)
by A30, FINSEQ_5:65;
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, Def4
.=
<*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(len f))
by A16, A10, A34, A35, A36, FINSEQ_6:132
.=
<*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(((len f) -' 1) + 1))
by A12, XREAL_1:237
.=
<*p*> ^ (Rev (mid f,1,(Index p,f)))
by A12, A5, A8, FINSEQ_6:119
.=
Rev ((mid f,1,(Index p,f)) ^ <*p*>)
by FINSEQ_5:66
.=
Rev (R_Cut f,p)
by A30, Def5
;
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:65;
A40:
now 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, Th53
.=
((Index p,f) + 1) + (Index p,(Rev f))
by A7
;
p =
f . (((len f) - ((Index p,(Rev f)) + 1)) + 1)
by A10, A41, FINSEQ_5:61
.=
f . ((Index p,f) + 1)
by A3, A42
;
hence
contradiction
by A38;
verum end; A43:
Index p,
f < len f
by A2, Th41;
len f = (Index p,(Rev f)) + (Index p,f)
by A1, A2, A38, Th54;
then Index p,
(Rev f) =
(len f) - (Index p,f)
.=
(len f) -' (Index p,f)
by A43, XREAL_1:235
;
hence L_Cut (Rev f),
p =
<*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(len f))
by A3, A40, Def4
.=
<*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(((len f) -' 1) + 1))
by A12, XREAL_1:237
.=
<*p*> ^ (Rev (mid f,1,(Index p,f)))
by A12, A5, A8, FINSEQ_6:119
.=
Rev ((mid f,1,(Index p,f)) ^ <*p*>)
by FINSEQ_5:66
.=
Rev (R_Cut f,p)
by A37, Def5
;
verum end;