let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) 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 (TOP-REAL 2); :: 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 A1, CARD_1:27, TOPREAL1:22;
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 A3, FINSEQ_5:6;
then A5: 1 <= len f by FINSEQ_3:25;
Index (p,f) < len f by A1, Th8;
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 A4, Def3;
hence (L_Cut (f,p)) . 1 = p by A4, A7, A6, A5, FINSEQ_6:118; :: 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 A8, FINSEQ_1:40;
A11: 1 <= (Index (p,f)) + 1 by NAT_1:11;
then A12: 1 <= len f by A2, XXREAL_0:2;
then len (mid (f,((Index (p,f)) + 1),(len f))) = ((len f) -' ((Index (p,f)) + 1)) + 1 by A11, A2, FINSEQ_6:118;
then A13: (len <*p*>) + (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 A2, XREAL_1:233
.= ((len f) - (Index (p,f))) + 1 ;
A14: (i -' 1) + 1 = (i - 1) + 1 by A8, XREAL_1:233
.= i ;
A15: 1 <= i - 1 by A8, SPPOL_1:1;
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 A8, A9, A11, A2, A12, FINSEQ_6:118
.= 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 <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) by A9, FINSEQ_1:22;
then i - 1 <= (((len f) - (Index (p,f))) + 1) - 1 by A13, XREAL_1:9;
then A19: i -' 1 <= ((len f) - ((Index (p,f)) + 1)) + 1 by A15, NAT_D:39;
len <*p*> < i by A8, FINSEQ_1:39;
then (L_Cut (f,p)) . i = (mid (f,((Index (p,f)) + 1),(len f))) . (i - (len <*p*>)) by A9, A18, FINSEQ_6:108
.= (mid (f,((Index (p,f)) + 1),(len f))) . (i -' (len <*p*>)) by A10, XREAL_1:233
.= (mid (f,((Index (p,f)) + 1),(len f))) . (i -' 1) by FINSEQ_1:39
.= f . (((i -' 1) + ((Index (p,f)) + 1)) -' 1) by A11, A2, A16, A19, FINSEQ_6:122
.= f . (((Index (p,f)) + i) -' 1) by A14 ;
hence (L_Cut (f,p)) . i = f . (((Index (p,f)) + i) - 1) by A8, A17, XREAL_1:233, XXREAL_0:2; :: thesis: verum