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 8;
then 1 <= len g by XXREAL_0:2;
then A4: len g in dom g by FINSEQ_3:25;
assume p in L~ g ; :: thesis: L_Cut (g,p) is_in_the_area_of f
then Index (p,g) < len g by JORDAN3:8;
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:25;

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 3;
mid (g,((Index (p,g)) + 1),(len g)) is_in_the_area_of f by A1, A4, A6, SPRECT_2:22;
hence L_Cut (g,p) is_in_the_area_of f by A2, A7, SPRECT_2:24; :: 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 3;
hence L_Cut (g,p) is_in_the_area_of f by A1, A4, A6, SPRECT_2:22; :: thesis: verum

end;

end;