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;

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) )
;

end;

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;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

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;hence L_Cut (g,p) is_in_the_area_of f by A1, A4, A6, SPRECT_2:22; :: thesis: verum