let f be S-Sequence_in_R2; :: thesis: for p being Point of (TOP-REAL 2) st p in rng f holds
R_Cut f,p = mid f,1,(p .. f)
let p be Point of (TOP-REAL 2); :: thesis: ( p in rng f implies R_Cut f,p = mid f,1,(p .. f) )
assume A1: p in rng f ; :: thesis: R_Cut f,p = mid f,1,(p .. f)
then consider i being Nat such that
A2: i in dom f and
A3: f . i = p by FINSEQ_2:11;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A4: ( 0 + 1 <= i & i <= len f ) by A2, FINSEQ_3:27;
then A5: i - 1 >= 0 by XREAL_1:21;
len f >= 2 by TOPREAL1:def 10;
then rng f c= L~ f by SPPOL_2:18;
then A6: ( 1 <= Index p,f & Index p,f < len f ) by A1, JORDAN3:41;

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

suppose A7: 1 < i ; :: thesis: R_Cut f,p = mid f,1,(p .. f)

then A8: (Index p,f) + 1 = i by A3, A4, JORDAN3:45;
1 <= len f by A4, XXREAL_0:2;
then 1 in dom f by FINSEQ_3:27;
then p <> f . 1 by A2, A3, A7, FUNCT_1:def 8;
then A9: R_Cut f,p = (mid f,1,(Index p,f)) ^ <*p*> by JORDAN3:def 5;
A10: len (mid f,1,i) = (i -' 1) + 1 by A4, JORDAN4:20
.= i by A4, XREAL_1:237 ;
A11: len (mid f,1,(Index p,f)) = ((Index p,f) -' 1) + 1 by A6, JORDAN4:20
.= i -' 1 by A6, A8, NAT_D:38 ;
then A12: len ((mid f,1,(Index p,f)) ^ <*p*>) = (i -' 1) + 1 by FINSEQ_2:19
.= i by A4, XREAL_1:237 ;
X: dom (mid f,1,i) = Seg i by A10, FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom (mid f,1,i) implies (mid f,1,i) . j = ((mid f,1,(Index p,f)) ^ <*p*>) . j )
assume j in dom (mid f,1,i) ; :: thesis: (mid f,1,i) . j = ((mid f,1,(Index p,f)) ^ <*p*>) . j
then A13: ( 1 <= j & j <= i ) by X, FINSEQ_1:3;
reconsider a = j as Element of NAT by ORDINAL1:def 13;

now

per cases ( j < i or j = i ) by A13, XXREAL_0:1;

suppose j < i ; :: thesis: (mid f,1,i) . j = ((mid f,1,(Index p,f)) ^ <*p*>) . j

then A14: j <= Index p,f by A8, NAT_1:13;
then j <= i -' 1 by A5, A8, XREAL_0:def 2;
then A15: j in dom (mid f,1,(Index p,f)) by A11, A13, FINSEQ_3:27;
thus (mid f,1,i) . j = f . a by A4, A13, JORDAN3:32
.= (mid f,1,(Index p,f)) . a by A6, A13, A14, JORDAN3:32
.= ((mid f,1,(Index p,f)) ^ <*p*>) . j by A15, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A16: j = i ; :: thesis: (mid f,1,i) . j = ((mid f,1,(Index p,f)) ^ <*p*>) . j

A17: (i -' 1) + 1 = i by A4, XREAL_1:237;
thus (mid f,1,i) . j = f . a by A4, A13, JORDAN3:32
.= ((mid f,1,(Index p,f)) ^ <*p*>) . j by A3, A11, A16, A17, FINSEQ_1:59 ; :: thesis: verum

end;

end;

end;

hence (mid f,1,i) . j = ((mid f,1,(Index p,f)) ^ <*p*>) . j ; :: thesis: verum

end;

then mid f,1,i = R_Cut f,p by A9, A10, A12, FINSEQ_2:10;
hence R_Cut f,p = mid f,1,(p .. f) by A2, A3, FINSEQ_5:12; :: thesis: verum

end;

suppose A18: 1 = i ; :: thesis: R_Cut f,p = mid f,1,(p .. f)

then A19: R_Cut f,p = <*p*> by A3, JORDAN3:def 5;
A20: p = f /. 1 by A2, A3, A18, PARTFUN1:def 8;
then p .. f = 1 by FINSEQ_6:47;
hence R_Cut f,p = mid f,1,(p .. f) by A4, A18, A19, A20, JORDAN4:27; :: thesis: verum

end;

end;