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) )
A1: len f >= 2 by TOPREAL1:def 10;
assume p in rng f ; :: thesis: L_Cut f,p = mid f,(p .. f),(len f)
then consider i being Nat such that
A2: i in dom f and
A3: f . i = p by FINSEQ_2:11;
A4: 0 + 1 <= i by A2, FINSEQ_3:27;
A5: i <= len f by A2, FINSEQ_3:27;

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

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

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

end;

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

thus L_Cut f,p = L_Cut f,(f /. i) by A2, A3, PARTFUN1:def 8
.= f by A7, JORDAN5B:30
.= mid f,1,(len f) by A1, FINSEQ_6:126, XXREAL_0:2
.= mid f,(p .. f),(len f) by A2, A3, A7, FINSEQ_5:12 ; :: thesis: verum

end;

end;