let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is special implies for p being Point of (TOP-REAL 2) st p in L~ f holds
R_Cut f,p is special )
assume A1: f is special ; :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
R_Cut f,p is special
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies R_Cut f,p is special )
A2: mid f,1,(Index p,f) is special by A1, Th27;
assume A3: p in L~ f ; :: thesis: R_Cut f,p is special
then A4: Index p,f < len f by JORDAN3:41;
len f <> 0 by A3, TOPREAL1:28;
then len f > 0 by NAT_1:3;
then len f >= 0 + 1 by NAT_1:13;
then A5: 1 in dom f by FINSEQ_3:27;
A6: 1 <= Index p,f by A3, JORDAN3:41;
then Index p,f in dom f by A4, FINSEQ_3:27;
then A7: (mid f,1,(Index p,f)) /. (len (mid f,1,(Index p,f))) = f /. (Index p,f) by A5, SPRECT_2:13;
(Index p,f) + 1 <= len f by A4, NAT_1:13;
then A8: LSeg f,(Index p,f) = LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A6, TOPREAL1:def 5;

A9: now

per cases ( LSeg f,(Index p,f) is vertical or LSeg f,(Index p,f) is horizontal ) by A1, SPPOL_1:41;

case LSeg f,(Index p,f) is vertical ; :: thesis: p `1 = (f /. (Index p,f)) `1

hence p `1 = (f /. (Index p,f)) `1 by A3, A8, JORDAN5B:32, SPPOL_1:64; :: thesis: verum

end;

case LSeg f,(Index p,f) is horizontal ; :: thesis: p `2 = (f /. (Index p,f)) `2

hence p `2 = (f /. (Index p,f)) `2 by A3, A8, JORDAN5B:32, SPPOL_1:63; :: thesis: verum

end;

end;

end;

A10: <*p*> /. 1 = p by FINSEQ_4:25;
A11: <*p*> is special by SPPOL_2:39;

per cases ( p <> f . 1 or p = f . 1 ) ;

suppose p <> f . 1 ; :: thesis: R_Cut f,p is special

then R_Cut f,p = (mid f,1,(Index p,f)) ^ <*p*> by JORDAN3:def 5;
hence R_Cut f,p is special by A11, A2, A10, A7, A9, GOBOARD2:13; :: thesis: verum

end;

suppose p = f . 1 ; :: thesis: R_Cut f,p is special

hence R_Cut f,p is special by A11, JORDAN3:def 5; :: thesis: verum

end;

end;