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 Th41;

now

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:35
.= (len (mid f,1,(Index p,f))) + 1 by FINSEQ_1:56 ;
R_Cut f,p = (mid f,1,(Index p,f)) ^ <*p*> by A3, Def5;
hence (R_Cut f,p) . (len (R_Cut f,p)) = p by A4, FINSEQ_1:59; :: 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 Def5;
then len (R_Cut f,p) = 1 by FINSEQ_1:57;
hence (R_Cut f,p) . (len (R_Cut f,p)) = p by A5, FINSEQ_1:57; :: 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, Th41;
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, Th27
.= Index p,f by A1, Th41, XREAL_1:237 ;
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

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 Def5
.= (mid f,1,(Index p,f)) . i by A7, A8, A9, FINSEQ_1:85
.= f . i by A2, A8, A9, Th32 ;
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:27;
then A12: p = f /. 1 by A10, PARTFUN1:def 8;
len f >= 1 + 1 by A11, NAT_1:13;
then Index p,f = 1 by A12, Th44;
then A13: i = 1 by A8, A9, XXREAL_0:1;
R_Cut f,p = <*p*> by A10, Def5;
hence (R_Cut f,p) . i = f . i by A10, A13, FINSEQ_1:57; :: thesis: verum

end;

end;

end;

hence (R_Cut f,p) . i = f . i ; :: thesis: verum

end;