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: i <= len f by A2, FINSEQ_3:27;
len f >= 2 by TOPREAL1:def 10;
then A5: rng f c= L~ f by SPPOL_2:18;
then A6: 1 <= Index p,f by A1, JORDAN3:41;
A7: Index p,f < len f by A1, A5, JORDAN3:41;
A8: 0 + 1 <= i by A2, FINSEQ_3:27;
then A9: i - 1 >= 0 by XREAL_1:21;

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

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

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

A16: 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 )
reconsider a = j as Element of NAT by ORDINAL1:def 13;
assume A17: j in dom (mid f,1,i) ; :: thesis: (mid f,1,i) . j = ((mid f,1,(Index p,f)) ^ <*p*>) . j
then A18: 1 <= j by A15, FINSEQ_1:3;
A19: j <= i by A15, A17, FINSEQ_1:3;

now

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

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

then A20: j <= Index p,f by A12, NAT_1:13;
then j <= i -' 1 by A9, A12, XREAL_0:def 2;
then A21: j in dom (mid f,1,(Index p,f)) by A13, A18, FINSEQ_3:27;
thus (mid f,1,i) . j = f . a by A4, A18, A19, FINSEQ_6:129
.= (mid f,1,(Index p,f)) . a by A7, A18, A20, FINSEQ_6:129
.= ((mid f,1,(Index p,f)) ^ <*p*>) . j by A21, FINSEQ_1:def 7 ; :: thesis: verum

end;

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

A23: (i -' 1) + 1 = i by A8, XREAL_1:237;
thus (mid f,1,i) . j = f . a by A4, A18, A19, FINSEQ_6:129
.= ((mid f,1,(Index p,f)) ^ <*p*>) . j by A3, A13, A22, A23, 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;

len ((mid f,1,(Index p,f)) ^ <*p*>) = (i -' 1) + 1 by A13, FINSEQ_2:19
.= i by A8, XREAL_1:237 ;
then mid f,1,i = R_Cut f,p by A11, A14, A16, FINSEQ_2:10;
hence R_Cut f,p = mid f,1,(p .. f) by A2, A3, FINSEQ_5:12; :: thesis: verum

end;

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

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

end;

end;