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 8;
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:10;
A4: 0 + 1 <= i by A2, FINSEQ_3:25;
A5: i <= len f by A2, FINSEQ_3:25;
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:12;
then L_Cut (f,p) = mid (f,((Index (p,f)) + 1),(len f)) by A3, JORDAN3:def 3;
hence L_Cut (f,p) = mid (f,(p .. f),(len f)) by A2, A3, A6, FINSEQ_5:11; :: 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 6
.= f by A7, JORDAN5B:27
.= mid (f,1,(len f)) by A1, FINSEQ_6:120, XXREAL_0:2
.= mid (f,(p .. f),(len f)) by A2, A3, A7, FINSEQ_5:11 ; :: thesis: verum
end;
end;