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
L_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 L_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 L_Cut g,p is_in_the_area_of f )
2 <= len g by A3, TOPREAL1:def 10;
then 1 <= len g by XXREAL_0:2;
then A4: len g in dom g by FINSEQ_3:27;
assume p in L~ g ; :: thesis: L_Cut g,p is_in_the_area_of f
then Index p,g < len g by JORDAN3:41;
then A5: (Index p,g) + 1 <= len g by NAT_1:13;
1 <= (Index p,g) + 1 by NAT_1:11;
then A6: (Index p,g) + 1 in dom g by A5, FINSEQ_3:27;

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

suppose p <> g . ((Index p,g) + 1) ; :: thesis: L_Cut g,p is_in_the_area_of f

then A7: L_Cut g,p = <*p*> ^ (mid g,((Index p,g) + 1),(len g)) by JORDAN3:def 4;
mid g,((Index p,g) + 1),(len g) is_in_the_area_of f by A1, A4, A6, SPRECT_2:26;
hence L_Cut g,p is_in_the_area_of f by A2, A7, SPRECT_2:28; :: thesis: verum

end;

suppose p = g . ((Index p,g) + 1) ; :: thesis: L_Cut g,p is_in_the_area_of f

then L_Cut g,p = mid g,((Index p,g) + 1),(len g) by JORDAN3:def 4;
hence L_Cut g,p is_in_the_area_of f by A1, A4, A6, SPRECT_2:26; :: thesis: verum

end;

end;