let f, g be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g holds
R_Cut g,p is_in_the_area_of f
let p be Point of (TOP-REAL 2); :: thesis: ( g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in L~ g implies R_Cut g,p is_in_the_area_of f )
assume that
A1: g is_in_the_area_of f and
A2: <*p*> is_in_the_area_of f and
A3: g is being_S-Seq ; :: thesis: ( not p in L~ g or R_Cut g,p is_in_the_area_of f )
2 <= len g by A3, TOPREAL1:def 10;
then A4: 1 <= len g by XXREAL_0:2;
then A5: 1 in dom g by FINSEQ_3:27;
assume A6: p in L~ g ; :: thesis: R_Cut g,p is_in_the_area_of f
then A7: Index p,g < len g by JORDAN3:41;
1 <= Index p,g by A6, JORDAN3:41;
then A8: Index p,g in dom g by A7, FINSEQ_3:27;

per cases ( p <> g . 1 or p = g . 1 ) ;

suppose p <> g . 1 ; :: thesis: R_Cut g,p is_in_the_area_of f

then A9: R_Cut g,p = (mid g,1,(Index p,g)) ^ <*p*> by JORDAN3:def 5;
mid g,1,(Index p,g) is_in_the_area_of f by A1, A5, A8, SPRECT_2:26;
hence R_Cut g,p is_in_the_area_of f by A2, A9, SPRECT_2:28; :: thesis: verum

end;

suppose p = g . 1 ; :: thesis: R_Cut g,p is_in_the_area_of f

then R_Cut g,p = <*(g . 1)*> by JORDAN3:def 5
.= <*(g /. 1)*> by A5, PARTFUN1:def 8
.= mid g,1,1 by A4, JORDAN4:27 ;
hence R_Cut g,p is_in_the_area_of f by A1, A5, SPRECT_2:26; :: thesis: verum

end;

end;