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;