let f, g be FinSequence of (); :: thesis: for p being Point of () 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 (); :: 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 ;
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 ;
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 ;
hence L_Cut (g,p) is_in_the_area_of f by ; :: 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 ; :: thesis: verum
end;
end;