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 8;
then 1 <= len g by XXREAL_0:2;
then A5: 1 in dom g by FINSEQ_3:25;
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:8;
1 <= Index (p,g) by A6, JORDAN3:8;
then A8: Index (p,g) in dom g by A7, FINSEQ_3:25;

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 4;
mid (g,1,(Index (p,g))) is_in_the_area_of f by A1, A5, A8, SPRECT_2:22;
hence R_Cut (g,p) is_in_the_area_of f by A2, A9, SPRECT_2:24; :: 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 4
.= mid (g,1,1) by A5, FINSEQ_6:193 ;
hence R_Cut (g,p) is_in_the_area_of f by A1, A5, SPRECT_2:22; :: thesis: verum

end;

end;