let f be FinSequence of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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;

f . 1 = p )

assume A1: f is being_S-Seq ; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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 )
;

end;

suppose
mid (f,((Index (p,f)) + 1),(len f)) is empty
; :: thesis: contradiction

then
L_Cut (f,p) = <*p*>
by A8, FINSEQ_1:34;

then len (L_Cut (f,p)) = 1 by FINSEQ_1:39;

hence contradiction by A5, TOPREAL1:22; :: thesis: verum

end;then len (L_Cut (f,p)) = 1 by FINSEQ_1:39;

hence contradiction by A5, TOPREAL1:22; :: thesis: verum

suppose
not mid (f,((Index (p,f)) + 1),(len f)) is empty
; :: thesis: contradiction

then
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; :: thesis: verum

end;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; :: thesis: verum