let f be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & Index p,f < Index q,f holds
q in L~ (L_Cut f,p)
let p, q be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & q in L~ f & Index p,f < Index q,f implies q in L~ (L_Cut f,p) )
assume that
A1:
p in L~ f
and
A2:
q in L~ f
and
A3:
Index p,f < Index q,f
; :: thesis: q in L~ (L_Cut f,p)
set i1 = ((Index q,f) -' (Index p,f)) + 1;
A4:
( 1 <= Index q,f & Index q,f < len f )
by A2, Th41;
A5:
(Index p,f) + 1 <= Index q,f
by A3, NAT_1:13;
then A6:
((Index p,f) + 1) - (Index p,f) <= (Index q,f) - (Index p,f)
by XREAL_1:11;
then A7:
1 <= (Index q,f) -' (Index p,f)
by XREAL_0:def 2;
then A8:
1 <= ((Index q,f) -' (Index p,f)) + 1
by NAT_D:48;
1 + 1 <= ((Index q,f) -' (Index p,f)) + 1
by A7, XREAL_1:8;
then A9:
1 < ((Index q,f) -' (Index p,f)) + 1
by XXREAL_0:2;
then A10:
len <*p*> < ((Index q,f) -' (Index p,f)) + 1
by FINSEQ_1:57;
then A11:
len <*p*> < (((Index q,f) -' (Index p,f)) + 1) + 1
by NAT_1:13;
A12:
( 1 <= (Index p,f) + 1 & (Index p,f) + 1 <= len f )
by A4, A5, NAT_1:11, XXREAL_0:2;
1 < len f
by A4, XXREAL_0:2;
then
len (mid f,((Index p,f) + 1),(len f)) = ((len f) -' ((Index p,f) + 1)) + 1
by A12, Th27;
then A13: (len <*p*>) + (len (mid f,((Index p,f) + 1),(len f))) =
1 + (((len f) -' ((Index p,f) + 1)) + 1)
by FINSEQ_1:57
.=
1 + (((len f) - ((Index p,f) + 1)) + 1)
by A12, XREAL_1:235
.=
((len f) - (Index p,f)) + 1
;
A14:
(Index q,f) - (Index p,f) <= (len f) - (Index p,f)
by A4, XREAL_1:11;
then A15:
((Index q,f) - (Index p,f)) + 1 <= ((len f) - (Index p,f)) + 1
by XREAL_1:8;
then A16:
((Index q,f) -' (Index p,f)) + 1 <= (len <*p*>) + (len (mid f,((Index p,f) + 1),(len f)))
by A3, A13, XREAL_1:235;
(Index q,f) - (Index p,f) <= (((len f) - (Index p,f)) - 1) + 1
by A4, XREAL_1:11;
then A17:
(Index q,f) -' (Index p,f) <= ((len f) - ((Index p,f) + 1)) + 1
by A3, XREAL_1:235;
per cases
( p = f . ((Index p,f) + 1) or p <> f . ((Index p,f) + 1) )
;
suppose A18:
p = f . ((Index p,f) + 1)
;
:: thesis: q in L~ (L_Cut f,p)then A19:
len (L_Cut f,p) = (len f) - (Index p,f)
by A1, Th61;
then
len (L_Cut f,p) >= (Index q,f) -' (Index p,f)
by A3, A14, XREAL_1:235;
then (L_Cut f,p) /. ((Index q,f) -' (Index p,f)) =
(L_Cut f,p) . ((Index q,f) -' (Index p,f))
by A7, FINSEQ_4:24
.=
(mid f,((Index p,f) + 1),(len f)) . ((Index q,f) -' (Index p,f))
by A18, Def4
.=
f . ((((Index p,f) + 1) + ((Index q,f) -' (Index p,f))) - 1)
by A7, A12, A17, Th31
.=
f . ((((Index p,f) + 1) + ((Index q,f) - (Index p,f))) - 1)
by A3, XREAL_1:235
.=
f . (Index q,f)
;
then A20:
(L_Cut f,p) /. ((Index q,f) -' (Index p,f)) = f /. (Index q,f)
by A4, FINSEQ_4:24;
A21:
Index q,
f < len f
by A2, Th41;
then A22:
(Index q,f) + 1
<= len f
by NAT_1:13;
then
((Index q,f) + 1) - (Index p,f) <= (len f) - (Index p,f)
by XREAL_1:11;
then
((Index q,f) - (Index p,f)) + 1
<= (len f) - (Index p,f)
;
then A23:
((Index q,f) -' (Index p,f)) + 1
<= len (L_Cut f,p)
by A6, A19, XREAL_0:def 2;
A24:
( 1
<= Index q,
f &
(Index q,f) + 1
<= len f &
q in LSeg f,
(Index q,f) )
by A2, A21, Th41, Th42, NAT_1:13;
A25:
((Index q,f) + 1) - (Index p,f) <= (len f) - (Index p,f)
by A22, XREAL_1:11;
then
((Index q,f) - (Index p,f)) + 1
<= (len f) - (Index p,f)
;
then A26:
len (L_Cut f,p) >= ((Index q,f) -' (Index p,f)) + 1
by A3, A19, XREAL_1:235;
((Index q,f) - (Index p,f)) + 1
<= (len f) - (Index p,f)
by A25;
then A27:
((Index q,f) -' (Index p,f)) + 1
<= ((len f) - ((Index p,f) + 1)) + 1
by A3, XREAL_1:235;
A28:
( 1
<= (Index q,f) + 1 &
(Index q,f) + 1
<= len f )
by A24, NAT_D:48;
A29:
(L_Cut f,p) /. (((Index q,f) -' (Index p,f)) + 1) =
(L_Cut f,p) . (((Index q,f) -' (Index p,f)) + 1)
by A9, A26, FINSEQ_4:24
.=
(mid f,((Index p,f) + 1),(len f)) . (((Index q,f) -' (Index p,f)) + 1)
by A18, Def4
.=
f . ((((Index p,f) + 1) + (((Index q,f) -' (Index p,f)) + 1)) - 1)
by A8, A12, A27, Th31
.=
f . ((((Index p,f) + 1) + (((Index q,f) - (Index p,f)) + 1)) - 1)
by A3, XREAL_1:235
.=
f /. ((Index q,f) + 1)
by A28, FINSEQ_4:24
;
q in LSeg f,
(Index q,f)
by A2, Th42;
then
q in LSeg ((L_Cut f,p) /. ((Index q,f) -' (Index p,f))),
((L_Cut f,p) /. (((Index q,f) -' (Index p,f)) + 1))
by A4, A20, A22, A29, TOPREAL1:def 5;
hence
q in L~ (L_Cut f,p)
by A7, A23, SPPOL_2:15;
:: thesis: verum end; suppose A30:
p <> f . ((Index p,f) + 1)
;
:: thesis: q in L~ (L_Cut f,p)A31:
len (L_Cut f,p) = ((len f) - (Index p,f)) + 1
by A1, A30, Th61;
then
len (L_Cut f,p) >= ((Index q,f) -' (Index p,f)) + 1
by A3, A15, XREAL_1:235;
then (L_Cut f,p) /. (((Index q,f) -' (Index p,f)) + 1) =
(L_Cut f,p) . (((Index q,f) -' (Index p,f)) + 1)
by FINSEQ_4:24, NAT_1:11
.=
(<*p*> ^ (mid f,((Index p,f) + 1),(len f))) . (((Index q,f) -' (Index p,f)) + 1)
by A30, Def4
.=
(mid f,((Index p,f) + 1),(len f)) . ((((Index q,f) -' (Index p,f)) + 1) - (len <*p*>))
by A10, A16, Th15
.=
(mid f,((Index p,f) + 1),(len f)) . ((((Index q,f) -' (Index p,f)) + 1) - 1)
by FINSEQ_1:57
.=
f . ((((Index p,f) + 1) + ((Index q,f) -' (Index p,f))) - 1)
by A7, A12, A17, Th31
.=
f . ((((Index p,f) + 1) + ((Index q,f) - (Index p,f))) - 1)
by A3, XREAL_1:235
.=
f . (Index q,f)
;
then A32:
(L_Cut f,p) /. (((Index q,f) -' (Index p,f)) + 1) = f /. (Index q,f)
by A4, FINSEQ_4:24;
A33:
Index q,
f < len f
by A2, Th41;
then A34:
(Index q,f) + 1
<= len f
by NAT_1:13;
then
((Index q,f) + 1) - (Index p,f) <= (len f) - (Index p,f)
by XREAL_1:11;
then
((Index q,f) - (Index p,f)) + 1
<= (len f) - (Index p,f)
;
then
((Index q,f) -' (Index p,f)) + 1
<= (len f) - (Index p,f)
by A6, XREAL_0:def 2;
then A35:
(((Index q,f) -' (Index p,f)) + 1) + 1
<= len (L_Cut f,p)
by A31, XREAL_1:8;
A36:
( 1
<= Index q,
f &
(Index q,f) + 1
<= len f &
q in LSeg f,
(Index q,f) )
by A2, A33, Th41, Th42, NAT_1:13;
A37:
((Index q,f) + 1) - (Index p,f) <= (len f) - (Index p,f)
by A34, XREAL_1:11;
then A38:
(((Index q,f) - (Index p,f)) + 1) + 1
<= ((len f) - (Index p,f)) + 1
by XREAL_1:8;
then A39:
len (L_Cut f,p) >= (((Index q,f) -' (Index p,f)) + 1) + 1
by A3, A31, XREAL_1:235;
A40:
(((Index q,f) -' (Index p,f)) + 1) + 1
<= (len <*p*>) + (len (mid f,((Index p,f) + 1),(len f)))
by A3, A13, A38, XREAL_1:235;
((Index q,f) - (Index p,f)) + 1
<= (len f) - (Index p,f)
by A37;
then A41:
((Index q,f) -' (Index p,f)) + 1
<= ((len f) - ((Index p,f) + 1)) + 1
by A3, XREAL_1:235;
A42:
( 1
<= (Index q,f) + 1 &
(Index q,f) + 1
<= len f )
by A36, NAT_D:48;
A43:
(L_Cut f,p) /. ((((Index q,f) -' (Index p,f)) + 1) + 1) =
(L_Cut f,p) . ((((Index q,f) -' (Index p,f)) + 1) + 1)
by A39, FINSEQ_4:24, NAT_1:11
.=
(<*p*> ^ (mid f,((Index p,f) + 1),(len f))) . ((((Index q,f) -' (Index p,f)) + 1) + 1)
by A30, Def4
.=
(mid f,((Index p,f) + 1),(len f)) . (((((Index q,f) -' (Index p,f)) + 1) + 1) - (len <*p*>))
by A11, A40, Th15
.=
(mid f,((Index p,f) + 1),(len f)) . (((((Index q,f) -' (Index p,f)) + 1) + 1) - 1)
by FINSEQ_1:57
.=
f . ((((Index p,f) + 1) + (((Index q,f) -' (Index p,f)) + 1)) - 1)
by A8, A12, A41, Th31
.=
f . ((((Index p,f) + 1) + (((Index q,f) - (Index p,f)) + 1)) - 1)
by A3, XREAL_1:235
.=
f /. ((Index q,f) + 1)
by A42, FINSEQ_4:24
;
q in LSeg f,
(Index q,f)
by A2, Th42;
then
q in LSeg ((L_Cut f,p) /. (((Index q,f) -' (Index p,f)) + 1)),
((L_Cut f,p) /. ((((Index q,f) -' (Index p,f)) + 1) + 1))
by A4, A32, A34, A43, TOPREAL1:def 5;
hence
q in L~ (L_Cut f,p)
by A35, NAT_1:11, SPPOL_2:15;
:: thesis: verum end;