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:
( f is unfolded & f is s.n.c. )
by A1;
A4:
Rev f is being_S-Seq
by A1, SPPOL_2:47;
then A5:
( Rev f is unfolded & Rev f is s.n.c. )
;
A6:
p in L~ (Rev f)
by A2, SPPOL_2:22;
A7:
Rev (Rev f) = f
by FINSEQ_6:29;
A8:
len f = len (Rev f)
by FINSEQ_5:def 3;
A9:
L~ f = L~ (Rev f)
by SPPOL_2:22;
A10:
dom (Rev f) = dom f
by FINSEQ_5:60;
A11:
1 <= (Index p,(Rev f)) + 1
by NAT_1:11;
Index p,(Rev f) < len (Rev f)
by A2, A9, Th41;
then A12:
(Index p,(Rev f)) + 1 <= len f
by A8, NAT_1:13;
then A13:
(Index p,(Rev f)) + 1 in dom f
by A11, FINSEQ_3:27;
A14:
1 + 1 <= len f
by A1, TOPREAL1:def 10;
then A15:
1 < len f
by NAT_1:13;
A16:
1 <= Index p,f
by A2, Th41;
A17:
Index p,f < len f
by A2, Th41;
A18:
1 in dom f
by A15, FINSEQ_3:27;
A19:
2 in dom f
by A14, FINSEQ_3:27;
A20:
len f in dom f
by A15, FINSEQ_3:27;
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 A21:
p = f . (len f)
;
:: thesis: L_Cut (Rev f),p = Rev (R_Cut f,p)then A22:
p = (Rev f) . 1
by FINSEQ_5:65;
then
p = (Rev f) /. 1
by A10, A18, PARTFUN1:def 8;
then A23:
Index p,
(Rev f) = 1
by A8, A14, Th44;
f is
one-to-one
by A1;
then A24:
p <> f . 1
by A15, A18, A20, A21, FUNCT_1:def 8;
Rev f is
one-to-one
by A4;
then A25:
p <> (Rev f) . (1 + 1)
by A10, A18, A19, A22, FUNCT_1:def 8;
then
(Index p,(Rev f)) + (Index p,f) = len f
by A5, A6, A7, A8, A23, Th54;
then A26:
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 A8, A23, A25, Def4
.=
<*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(len f))
by A17, A26, XREAL_1:235
.=
<*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(((len f) -' 1) + 1))
by A15, XREAL_1:237
.=
<*p*> ^ (Rev (mid f,1,(Index p,f)))
by A15, A16, A17, Th22
.=
Rev ((mid f,1,(Index p,f)) ^ <*p*>)
by FINSEQ_5:66
.=
Rev (R_Cut f,p)
by A24, Def5
;
:: thesis: verum end; suppose A27:
p = f . 1
;
:: thesis: L_Cut (Rev f),p = Rev (R_Cut f,p)then A28:
p = (Rev f) . (len f)
by FINSEQ_5:65;
A29:
len ((Rev f) /^ ((len (Rev f)) -' 1)) = (len (Rev f)) -' ((len (Rev f)) -' 1)
by RFINSEQ:42;
A30:
((len (Rev f)) -' 1) + 1
= len (Rev f)
by A8, A15, XREAL_1:237;
then A31:
((Rev f) /^ ((len (Rev f)) -' 1)) . 1
= (Rev f) . (len (Rev f))
by Th23;
1
<= (len (Rev f)) - ((len (Rev f)) -' 1)
by A30;
then A32:
1
<= len ((Rev f) /^ ((len (Rev f)) -' 1))
by A29, NAT_D:39;
then A33:
not
(Rev f) /^ ((len (Rev f)) -' 1) is
empty
by CARD_1:47;
((len (Rev f)) -' (len (Rev f))) + 1 =
((len (Rev f)) - (len (Rev f))) + 1
by XREAL_1:235
.=
1
;
then A34:
mid (Rev f),
(len (Rev f)),
(len (Rev f)) =
((Rev f) /^ ((len (Rev f)) -' 1)) | 1
by Def1
.=
<*(((Rev f) /^ ((len (Rev f)) -' 1)) /. 1)*>
by A33, FINSEQ_5:23
.=
<*((Rev f) . (len (Rev f)))*>
by A31, A32, FINSEQ_4:24
;
(Index p,(Rev f)) + 1
= len f
by A1, A8, A15, A28, Th45, SPPOL_2:47;
hence L_Cut (Rev f),
p =
<*p*>
by A8, A28, A34, Def4
.=
Rev <*p*>
by FINSEQ_5:63
.=
Rev (R_Cut f,p)
by A27, Def5
;
:: thesis: verum end; suppose that A35:
p <> f . 1
and A36:
p <> f . (len f)
and A37:
p = f . ((Index p,f) + 1)
;
:: thesis: L_Cut (Rev f),p = Rev (R_Cut f,p)A38:
p <> (Rev f) . (len f)
by A35, FINSEQ_5:65;
len f =
((Index p,(Rev f)) + (Index p,f)) + 1
by A1, A2, A36, A37, Th53
.=
(Index p,(Rev f)) + ((Index p,f) + 1)
;
then A39:
p =
f . (((len f) - ((Index p,(Rev f)) + 1)) + 1)
by A37
.=
(Rev f) . ((Index p,(Rev f)) + 1)
by A13, FINSEQ_5:61
;
A40:
len f =
((Index p,(Rev f)) + (Index p,f)) + 1
by A1, A2, A36, A37, Th53
.=
(Index p,f) + ((Index p,(Rev f)) + 1)
;
A41:
(len f) -' (Index p,f) =
(len f) - (Index p,f)
by A17, XREAL_1:235
.=
(Index p,(Rev f)) + 1
by A40
;
A42:
(Index p,(Rev f)) + 1
< len f
by A12, A38, A39, XXREAL_0:1;
thus L_Cut (Rev f),
p =
mid (Rev f),
((Index p,(Rev f)) + 1),
(len f)
by A8, A39, Def4
.=
<*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(len f))
by A10, A13, A39, A41, A42, Th56
.=
<*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(((len f) -' 1) + 1))
by A15, XREAL_1:237
.=
<*p*> ^ (Rev (mid f,1,(Index p,f)))
by A15, A16, A17, Th22
.=
Rev ((mid f,1,(Index p,f)) ^ <*p*>)
by FINSEQ_5:66
.=
Rev (R_Cut f,p)
by A35, Def5
;
:: thesis: verum end; suppose that A43:
p <> f . 1
and A44:
p <> f . ((Index p,f) + 1)
;
:: thesis: L_Cut (Rev f),p = Rev (R_Cut f,p)A45:
p <> (Rev f) . (len f)
by A43, FINSEQ_5:65;
A46:
now assume A47:
p = (Rev f) . ((Index p,(Rev f)) + 1)
;
:: thesis: contradictionthen A48:
len (Rev f) =
((Index p,(Rev (Rev f))) + (Index p,(Rev f))) + 1
by A1, A6, A8, A45, Th53, SPPOL_2:47
.=
((Index p,f) + 1) + (Index p,(Rev f))
by A7
;
p =
f . (((len f) - ((Index p,(Rev f)) + 1)) + 1)
by A13, A47, FINSEQ_5:61
.=
f . ((Index p,f) + 1)
by A8, A48
;
hence
contradiction
by A44;
:: thesis: verum end; A49:
len f = (Index p,(Rev f)) + (Index p,f)
by A2, A3, A44, Th54;
A50:
Index p,
f < len f
by A2, Th41;
Index p,
(Rev f) =
(len f) - (Index p,f)
by A49
.=
(len f) -' (Index p,f)
by A50, XREAL_1:235
;
hence L_Cut (Rev f),
p =
<*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(len f))
by A8, A46, Def4
.=
<*p*> ^ (mid (Rev f),(((len f) -' (Index p,f)) + 1),(((len f) -' 1) + 1))
by A15, XREAL_1:237
.=
<*p*> ^ (Rev (mid f,1,(Index p,f)))
by A15, A16, A17, Th22
.=
Rev ((mid f,1,(Index p,f)) ^ <*p*>)
by FINSEQ_5:66
.=
Rev (R_Cut f,p)
by A43, Def5
;
:: thesis: verum end;