let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
( (R_Cut (f,p)) . (len (R_Cut (f,p))) = p & ( for i being Element of NAT st 1 <= i & i <= Index (p,f) holds
(R_Cut (f,p)) . i = f . i ) )
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies ( (R_Cut (f,p)) . (len (R_Cut (f,p))) = p & ( for i being Element of NAT st 1 <= i & i <= Index (p,f) holds
(R_Cut (f,p)) . i = f . i ) ) )
assume A1: p in L~ f ; :: thesis: ( (R_Cut (f,p)) . (len (R_Cut (f,p))) = p & ( for i being Element of NAT st 1 <= i & i <= Index (p,f) holds
(R_Cut (f,p)) . i = f . i ) )
then A2: Index (p,f) < len f by Th8;
now :: thesis: (R_Cut (f,p)) . (len (R_Cut (f,p))) = p
per cases ( p <> f . 1 or p = f . 1 ) ;
suppose A3: p <> f . 1 ; :: thesis: (R_Cut (f,p)) . (len (R_Cut (f,p))) = p
A4: len ((mid (f,1,(Index (p,f)))) ^ <*p*>) = (len (mid (f,1,(Index (p,f))))) + (len <*p*>) by FINSEQ_1:22
.= (len (mid (f,1,(Index (p,f))))) + 1 by FINSEQ_1:39 ;
R_Cut (f,p) = (mid (f,1,(Index (p,f)))) ^ <*p*> by A3, Def4;
hence (R_Cut (f,p)) . (len (R_Cut (f,p))) = p by A4, FINSEQ_1:42; :: thesis: verum
end;
suppose p = f . 1 ; :: thesis: (R_Cut (f,p)) . (len (R_Cut (f,p))) = p
then A5: R_Cut (f,p) = <*p*> by Def4;
then len (R_Cut (f,p)) = 1 by FINSEQ_1:40;
hence (R_Cut (f,p)) . (len (R_Cut (f,p))) = p by A5, FINSEQ_1:40; :: thesis: verum
end;
end;
end;
hence (R_Cut (f,p)) . (len (R_Cut (f,p))) = p ; :: thesis: for i being Element of NAT st 1 <= i & i <= Index (p,f) holds
(R_Cut (f,p)) . i = f . i
A6: 1 <= Index (p,f) by A1, Th8;
then len f > 1 by A2, XXREAL_0:2;
then A7: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by A6, A2, FINSEQ_6:118
.= Index (p,f) by A1, Th8, XREAL_1:235 ;
thus for i being Element of NAT st 1 <= i & i <= Index (p,f) holds
(R_Cut (f,p)) . i = f . i :: thesis: verum
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= Index (p,f) implies (R_Cut (f,p)) . i = f . i )
assume that
A8: 1 <= i and
A9: i <= Index (p,f) ; :: thesis: (R_Cut (f,p)) . i = f . i
now :: thesis: ( ( p <> f . 1 & (R_Cut (f,p)) . i = f . i ) or ( p = f . 1 & (R_Cut (f,p)) . i = f . i ) )
per cases ( p <> f . 1 or p = f . 1 ) ;
case p <> f . 1 ; :: thesis: (R_Cut (f,p)) . i = f . i
then (R_Cut (f,p)) . i = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . i by Def4
.= (mid (f,1,(Index (p,f)))) . i by A7, A8, A9, FINSEQ_1:64
.= f . i by A2, A8, A9, FINSEQ_6:123 ;
hence (R_Cut (f,p)) . i = f . i ; :: thesis: verum
end;
case A10: p = f . 1 ; :: thesis: (R_Cut (f,p)) . i = f . i
A11: len f > 1 by A6, A2, XXREAL_0:2;
then 1 in dom f by FINSEQ_3:25;
then A12: p = f /. 1 by A10, PARTFUN1:def 6;
len f >= 1 + 1 by A11, NAT_1:13;
then Index (p,f) = 1 by A12, Th11;
then A13: i = 1 by A8, A9, XXREAL_0:1;
R_Cut (f,p) = <*p*> by A10, Def4;
hence (R_Cut (f,p)) . i = f . i by A10, A13, FINSEQ_1:40; :: thesis: verum
end;
end;
end;
hence (R_Cut (f,p)) . i = f . i ; :: thesis: verum
end;