let f be FinSequence of (); :: thesis: for p being Point of () st p in L~ f holds
( (L_Cut (f,p)) . 1 = p & ( for i being Nat st 1 < i & i <= len (L_Cut (f,p)) holds
( ( p = f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . ((Index (p,f)) + i) ) & ( p <> f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . (((Index (p,f)) + i) - 1) ) ) ) )

let p be Point of (); :: thesis: ( p in L~ f implies ( (L_Cut (f,p)) . 1 = p & ( for i being Nat st 1 < i & i <= len (L_Cut (f,p)) holds
( ( p = f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . ((Index (p,f)) + i) ) & ( p <> f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . (((Index (p,f)) + i) - 1) ) ) ) ) )

assume A1: p in L~ f ; :: thesis: ( (L_Cut (f,p)) . 1 = p & ( for i being Nat st 1 < i & i <= len (L_Cut (f,p)) holds
( ( p = f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . ((Index (p,f)) + i) ) & ( p <> f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . (((Index (p,f)) + i) - 1) ) ) ) )

then Index (p,f) < len f by Th8;
then A2: (Index (p,f)) + 1 <= len f by NAT_1:13;
A3: not f is empty by ;
now :: thesis: (L_Cut (f,p)) . 1 = p
per cases ( p = f . ((Index (p,f)) + 1) or p <> f . ((Index (p,f)) + 1) ) ;
suppose A4: p = f . ((Index (p,f)) + 1) ; :: thesis: (L_Cut (f,p)) . 1 = p
1 in dom f by ;
then A5: 1 <= len f by FINSEQ_3:25;
Index (p,f) < len f by ;
then A6: (Index (p,f)) + 1 <= len f by NAT_1:13;
A7: 1 <= (Index (p,f)) + 1 by NAT_1:11;
L_Cut (f,p) = mid (f,((Index (p,f)) + 1),(len f)) by ;
hence (L_Cut (f,p)) . 1 = p by ; :: thesis: verum
end;
suppose p <> f . ((Index (p,f)) + 1) ; :: thesis: (L_Cut (f,p)) . 1 = p
then L_Cut (f,p) = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) by Def3;
hence (L_Cut (f,p)) . 1 = p by FINSEQ_1:41; :: thesis: verum
end;
end;
end;
hence (L_Cut (f,p)) . 1 = p ; :: thesis: for i being Nat st 1 < i & i <= len (L_Cut (f,p)) holds
( ( p = f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . ((Index (p,f)) + i) ) & ( p <> f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . (((Index (p,f)) + i) - 1) ) )

let i be Nat; :: thesis: ( 1 < i & i <= len (L_Cut (f,p)) implies ( ( p = f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . ((Index (p,f)) + i) ) & ( p <> f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . (((Index (p,f)) + i) - 1) ) ) )
assume that
A8: 1 < i and
A9: i <= len (L_Cut (f,p)) ; :: thesis: ( ( p = f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . ((Index (p,f)) + i) ) & ( p <> f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . (((Index (p,f)) + i) - 1) ) )
A10: len <*p*> <= i by ;
A11: 1 <= (Index (p,f)) + 1 by NAT_1:11;
then A12: 1 <= len f by ;
then len (mid (f,((Index (p,f)) + 1),(len f))) = ((len f) -' ((Index (p,f)) + 1)) + 1 by ;
then A13: () + (len (mid (f,((Index (p,f)) + 1),(len f)))) = 1 + (((len f) -' ((Index (p,f)) + 1)) + 1) by FINSEQ_1:40
.= 1 + (((len f) - ((Index (p,f)) + 1)) + 1) by
.= ((len f) - (Index (p,f))) + 1 ;
A14: (i -' 1) + 1 = (i - 1) + 1 by
.= i ;
A15: 1 <= i - 1 by ;
then A16: 1 <= i -' 1 by NAT_D:39;
hereby :: thesis: ( p <> f . ((Index (p,f)) + 1) implies (L_Cut (f,p)) . i = f . (((Index (p,f)) + i) - 1) )
assume p = f . ((Index (p,f)) + 1) ; :: thesis: (L_Cut (f,p)) . i = f . ((Index (p,f)) + i)
then L_Cut (f,p) = mid (f,((Index (p,f)) + 1),(len f)) by Def3;
hence (L_Cut (f,p)) . i = f . ((i + ((Index (p,f)) + 1)) -' 1) by
.= f . (((i + (Index (p,f))) + 1) -' 1)
.= f . ((Index (p,f)) + i) by NAT_D:34 ;
:: thesis: verum
end;
A17: i <= i + (Index (p,f)) by NAT_1:11;
assume p <> f . ((Index (p,f)) + 1) ; :: thesis: (L_Cut (f,p)) . i = f . (((Index (p,f)) + i) - 1)
then A18: L_Cut (f,p) = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) by Def3;
then i <= () + (len (mid (f,((Index (p,f)) + 1),(len f)))) by ;
then i - 1 <= (((len f) - (Index (p,f))) + 1) - 1 by ;
then A19: i -' 1 <= ((len f) - ((Index (p,f)) + 1)) + 1 by ;
len <*p*> < i by ;
then (L_Cut (f,p)) . i = (mid (f,((Index (p,f)) + 1),(len f))) . (i - ()) by
.= (mid (f,((Index (p,f)) + 1),(len f))) . (i -' ()) by
.= (mid (f,((Index (p,f)) + 1),(len f))) . (i -' 1) by FINSEQ_1:39
.= f . (((i -' 1) + ((Index (p,f)) + 1)) -' 1) by
.= f . (((Index (p,f)) + i) -' 1) by A14 ;
hence (L_Cut (f,p)) . i = f . (((Index (p,f)) + i) - 1) by ; :: thesis: verum