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:8;
len f <> 0 by A3, TOPREAL1:22;
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:25;
A6: 1 <= Index (p,f) by A3, JORDAN3:8;
then Index (p,f) in dom f by A4, FINSEQ_3:25;
then A7: (mid (f,1,(Index (p,f)))) /. (len (mid (f,1,(Index (p,f))))) = f /. (Index (p,f)) by A5, SPRECT_2:9;
(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 3;

A9: now :: thesis: ( ( LSeg (f,(Index (p,f))) is vertical & p `1 = (f /. (Index (p,f))) `1 ) or ( LSeg (f,(Index (p,f))) is horizontal & p `2 = (f /. (Index (p,f))) `2 ) )

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

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:29, SPPOL_1:41; :: 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:29, SPPOL_1:40; :: thesis: verum

end;

end;

end;

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

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 4;
hence R_Cut (f,p) is special by A2, A10, A7, A9, GOBOARD2:8; :: 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 4; :: thesis: verum

end;

end;