let f be non empty FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) holds
L_Cut ((Rev f),p) = Rev (R_Cut (f,p))
let p be Point of (TOP-REAL 2); ( f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) implies L_Cut ((Rev f),p) = Rev (R_Cut (f,p)) )
assume that
A1:
( f is poorly-one-to-one & f is unfolded & f is s.n.c. )
and
A2:
p in L~ f
and
A3:
p <> f . (len f)
; L_Cut ((Rev f),p) = Rev (R_Cut (f,p))
A4:
Index (p,f) < len f
by A2, JORDAN3:8;
A5:
p in L~ (Rev f)
by A2, SPPOL_2:22;
A6:
Rev f is s.n.c.
by A1, SPPOL_2:35;
A7:
dom (Rev f) = dom f
by FINSEQ_5:57;
A8:
len f = len (Rev f)
by FINSEQ_5:def 3;
A9:
1 <= Index (p,f)
by A2, JORDAN3:8;
then A10:
1 < len f
by A4, XXREAL_0:2;
L~ f = L~ (Rev f)
by SPPOL_2:22;
then
Index (p,(Rev f)) < len (Rev f)
by A2, JORDAN3:8;
then A11:
(Index (p,(Rev f))) + 1 <= len f
by A8, NAT_1:13;
1 <= (Index (p,(Rev f))) + 1
by NAT_1:11;
then A12:
(Index (p,(Rev f))) + 1 in dom f
by A11, FINSEQ_3:25;
per cases
( 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) ) )
by A3;
suppose A13:
p = f . 1
;
L_Cut ((Rev f),p) = Rev (R_Cut (f,p))A14:
((len (Rev f)) -' 1) + 1
= len (Rev f)
by A8, A9, A4, XREAL_1:235, XXREAL_0:2;
then A15:
((Rev f) /^ ((len (Rev f)) -' 1)) . 1
= (Rev f) . (len (Rev f))
by FINSEQ_6:114;
A16:
len ((Rev f) /^ ((len (Rev f)) -' 1)) = (len (Rev f)) -' ((len (Rev f)) -' 1)
by RFINSEQ:29;
A17:
1
<= (len (Rev f)) - ((len (Rev f)) -' 1)
by A14;
A19:
not
(Rev f) /^ ((len (Rev f)) -' 1) is
empty
by A16, A17, NAT_D:39;
((len (Rev f)) -' (len (Rev f))) + 1 =
((len (Rev f)) - (len (Rev f))) + 1
by XREAL_1:233
.=
1
;
then A20:
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 A19, FINSEQ_5:20
.=
<*((Rev f) . (len (Rev f)))*>
by A15
;
A21:
p = (Rev f) . (len f)
by A13, FINSEQ_5:62;
then
(Index (p,(Rev f))) + 1
= len f
by A1, A6, A8, A10, Th18, SPPOL_2:28;
hence L_Cut (
(Rev f),
p) =
<*p*>
by A8, A21, A20, JORDAN3:def 3
.=
Rev <*p*>
by FINSEQ_5:60
.=
Rev (R_Cut (f,p))
by A13, JORDAN3:def 4
;
verum end; suppose that A22:
p <> f . 1
and A23:
p <> f . (len f)
and A24:
p = f . ((Index (p,f)) + 1)
;
L_Cut ((Rev f),p) = Rev (R_Cut (f,p))A25:
len f =
((Index (p,(Rev f))) + (Index (p,f))) + 1
by A1, A2, A23, A24, Th36
.=
(Index (p,f)) + ((Index (p,(Rev f))) + 1)
;
len f =
((Index (p,(Rev f))) + (Index (p,f))) + 1
by A1, A2, A23, A24, Th36
.=
(Index (p,(Rev f))) + ((Index (p,f)) + 1)
;
then A26:
p =
f . (((len f) - ((Index (p,(Rev f))) + 1)) + 1)
by A24
.=
(Rev f) . ((Index (p,(Rev f))) + 1)
by A12, FINSEQ_5:58
;
A27:
(len f) -' (Index (p,f)) =
(len f) - (Index (p,f))
by A4, XREAL_1:233
.=
(Index (p,(Rev f))) + 1
by A25
;
p <> (Rev f) . (len f)
by A22, FINSEQ_5:62;
then A28:
(Index (p,(Rev f))) + 1
< len f
by A11, A26, XXREAL_0:1;
thus L_Cut (
(Rev f),
p) =
mid (
(Rev f),
((Index (p,(Rev f))) + 1),
(len f))
by A8, A26, JORDAN3:def 3
.=
<*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(len f)))
by A7, A12, A26, A27, A28, FINSEQ_6:126
.=
<*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(((len f) -' 1) + 1)))
by A9, A4, XREAL_1:235, XXREAL_0:2
.=
<*p*> ^ (Rev (mid (f,1,(Index (p,f)))))
by A9, A4, A10, FINSEQ_6:113
.=
Rev ((mid (f,1,(Index (p,f)))) ^ <*p*>)
by FINSEQ_5:63
.=
Rev (R_Cut (f,p))
by A22, JORDAN3:def 4
;
verum end; suppose that A29:
p <> f . 1
and A30:
p <> f . ((Index (p,f)) + 1)
;
L_Cut ((Rev f),p) = Rev (R_Cut (f,p))A31:
p <> (Rev f) . (len f)
by A29, FINSEQ_5:62;
A32:
now not p = (Rev f) . ((Index (p,(Rev f))) + 1)assume A33:
p = (Rev f) . ((Index (p,(Rev f))) + 1)
;
contradictionthen A34:
len (Rev f) =
((Index (p,(Rev (Rev f)))) + (Index (p,(Rev f)))) + 1
by A1, A6, A5, A8, A31, Th36, SPPOL_2:28
.=
((Index (p,f)) + 1) + (Index (p,(Rev f)))
;
p =
f . (((len f) - ((Index (p,(Rev f))) + 1)) + 1)
by A12, A33, FINSEQ_5:58
.=
f . ((Index (p,f)) + 1)
by A8, A34
;
hence
contradiction
by A30;
verum end; A35:
Index (
p,
f)
< len f
by A2, JORDAN3:8;
len f = (Index (p,(Rev f))) + (Index (p,f))
by A1, A2, A30, JORDAN3:21;
then Index (
p,
(Rev f)) =
(len f) - (Index (p,f))
.=
(len f) -' (Index (p,f))
by A35, XREAL_1:233
;
hence L_Cut (
(Rev f),
p) =
<*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(len f)))
by A8, A32, JORDAN3:def 3
.=
<*p*> ^ (mid ((Rev f),(((len f) -' (Index (p,f))) + 1),(((len f) -' 1) + 1)))
by A9, A4, XREAL_1:235, XXREAL_0:2
.=
<*p*> ^ (Rev (mid (f,1,(Index (p,f)))))
by A9, A4, A10, FINSEQ_6:113
.=
Rev ((mid (f,1,(Index (p,f)))) ^ <*p*>)
by FINSEQ_5:63
.=
Rev (R_Cut (f,p))
by A29, JORDAN3:def 4
;
verum end; end;