let f be FinSequence of (); :: thesis: ( f is being_S-Seq implies for p being Point of () 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 () st p in L~ f & f . 1 in L~ (L_Cut (f,p)) holds
f . 1 = p

A2: len f in dom f by ;
1 in dom f by ;
then A3: f /. 1 = f . 1 by PARTFUN1:def 6;
let p be Point of (); :: 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 ;
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 mid (f,((Index (p,f)) + 1),(len f)) is empty ; :: thesis: contradiction
end;
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 ;
then A9: f . 1 in LSeg (p,((mid (f,((Index (p,f)) + 1),(len f))) /. 1)) by ;
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 ;
LSeg ((<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))),i) c= LSeg (f,(((Index (p,f)) + i) -' 1)) by ;
then A15: ((Index (p,f)) + i) -' 1 = 1 by ;
A16: 1 <= Index (p,f) by ;
then 1 + 1 <= (Index (p,f)) + i by ;
then A17: (Index (p,f)) + i = 1 + 1 by ;
then Index (p,f) = 1 by ;
then p in LSeg (f,1) by ;
then A18: p in LSeg ((f /. 1),(f /. (1 + 1))) by ;
i = 1 by A12, A16, A17, Th6;
then (mid (f,((Index (p,f)) + 1),(len f))) /. 1 = f /. (1 + 1) by ;
hence contradiction by A6, A3, A9, A18, SPRECT_3:6; :: thesis: verum
end;
end;