let f be S-Sequence_in_R2; :: thesis: for p being Point of (TOP-REAL 2) st p in rng f holds
L_Cut f,p = mid f,(p .. f),(len f)
let p be Point of (TOP-REAL 2); :: thesis: ( p in rng f implies L_Cut f,p = mid f,(p .. f),(len f) )
assume p in rng f ; :: thesis: L_Cut f,p = mid f,(p .. f),(len f)
then consider i being Nat such that
A1: i in dom f and
A2: f . i = p by FINSEQ_2:11;
A3: ( 0 + 1 <= i & i <= len f ) by A1, FINSEQ_3:27;
A4: len f >= 2 by TOPREAL1:def 10;

per cases ( i > 1 or i = 1 ) by A3, XXREAL_0:1;

suppose i > 1 ; :: thesis: L_Cut f,p = mid f,(p .. f),(len f)

then A5: (Index p,f) + 1 = i by A2, A3, JORDAN3:45;
then L_Cut f,p = mid f,((Index p,f) + 1),(len f) by A2, JORDAN3:def 4;
hence L_Cut f,p = mid f,(p .. f),(len f) by A1, A2, A5, FINSEQ_5:12; :: thesis: verum

end;

suppose A6: i = 1 ; :: thesis: L_Cut f,p = mid f,(p .. f),(len f)

thus L_Cut f,p = L_Cut f,(f /. i) by A1, A2, PARTFUN1:def 8
.= f by A6, JORDAN5B:30
.= mid f,1,(len f) by A4, JORDAN3:29, XXREAL_0:2
.= mid f,(p .. f),(len f) by A1, A2, A6, FINSEQ_5:12 ; :: thesis: verum

end;

end;