let f be FinSequence of (TOP-REAL 2); ( f is being_S-Seq implies for p being Point of (TOP-REAL 2) st p in L~ f & f . 1 in L~ (L_Cut (f,p)) holds
f . 1 = p )
assume A1:
f is being_S-Seq
; for p being Point of (TOP-REAL 2) st p in L~ f & f . 1 in L~ (L_Cut (f,p)) holds
f . 1 = p
A2:
len f in dom f
by A1, FINSEQ_5:6;
1 in dom f
by A1, FINSEQ_5:6;
then A3:
f /. 1 = f . 1
by PARTFUN1:def 6;
let p be Point of (TOP-REAL 2); ( p in L~ f & f . 1 in L~ (L_Cut (f,p)) implies f . 1 = p )
assume that
A4:
p in L~ f
and
A5:
f . 1 in L~ (L_Cut (f,p))
and
A6:
f . 1 <> p
; contradiction
set g = mid (f,((Index (p,f)) + 1),(len f));
A7:
not f . 1 in L~ (mid (f,((Index (p,f)) + 1),(len f)))
by A1, A4, Th5;
then
p <> f . ((Index (p,f)) + 1)
by A5, JORDAN3:def 3;
then A8:
L_Cut (f,p) = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))
by JORDAN3:def 3;
per cases
( mid (f,((Index (p,f)) + 1),(len f)) is empty or not mid (f,((Index (p,f)) + 1),(len f)) is empty )
;
suppose
not
mid (
f,
((Index (p,f)) + 1),
(len f)) is
empty
;
contradictionthen
L~ (L_Cut (f,p)) = (LSeg (p,((mid (f,((Index (p,f)) + 1),(len f))) /. 1))) \/ (L~ (mid (f,((Index (p,f)) + 1),(len f))))
by A8, SPPOL_2:20;
then A9:
f . 1
in LSeg (
p,
((mid (f,((Index (p,f)) + 1),(len f))) /. 1))
by A5, A7, XBOOLE_0:def 3;
A10:
1
+ 1
<= len f
by A1;
then A11:
2
in dom f
by FINSEQ_3:25;
consider i being
Nat such that A12:
1
<= i
and A13:
i + 1
<= len (<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))))
and A14:
f /. 1
in LSeg (
(<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))),
i)
by A5, A3, A8, SPPOL_2:13;
LSeg (
(<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))),
i)
c= LSeg (
f,
(((Index (p,f)) + i) -' 1))
by A4, A12, A13, JORDAN3:16;
then A15:
((Index (p,f)) + i) -' 1
= 1
by A1, A14, JORDAN5B:30;
A16:
1
<= Index (
p,
f)
by A4, JORDAN3:8;
then
1
+ 1
<= (Index (p,f)) + i
by A12, XREAL_1:7;
then A17:
(Index (p,f)) + i = 1
+ 1
by A15, XREAL_1:235, XXREAL_0:2;
then
Index (
p,
f)
= 1
by A12, A16, Th6;
then
p in LSeg (
f,1)
by A4, JORDAN3:9;
then A18:
p in LSeg (
(f /. 1),
(f /. (1 + 1)))
by A10, TOPREAL1:def 3;
i = 1
by A12, A16, A17, Th6;
then
(mid (f,((Index (p,f)) + 1),(len f))) /. 1
= f /. (1 + 1)
by A2, A17, A11, SPRECT_2:8;
hence
contradiction
by A6, A3, A9, A18, SPRECT_3:6;
verum end; end;