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
L_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
L_Cut f,p is special
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies L_Cut f,p is special )
assume A2: p in L~ f ; :: thesis: L_Cut f,p is special
A3: <*p*> is special by SPPOL_2:39;
len f <> 0 by A2, TOPREAL1:28;
then len f > 0 by NAT_1:3;
then A4: len f >= 0 + 1 by NAT_1:13;
A5: (Index p,f) + 1 >= 1 by NAT_1:11;
A6: mid f,((Index p,f) + 1),(len f) is special by A1, Th27;
A7: len <*p*> = 1 by FINSEQ_1:56;
A8: <*p*> /. 1 = p by FINSEQ_4:25;
A9: ( 1 <= Index p,f & Index p,f < len f ) by A2, JORDAN3:41;
then A10: (Index p,f) + 1 <= len f by NAT_1:13;
then ( (Index p,f) + 1 in dom f & len f in dom f ) by A4, A5, FINSEQ_3:27;
then A11: (mid f,((Index p,f) + 1),(len f)) /. 1 = f /. ((Index p,f) + 1) by SPRECT_2:12;
A12: LSeg f,(Index p,f) = LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A9, A10, TOPREAL1:def 5;

A13: 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)) `1

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

end;

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

hence p `2 = (f /. ((Index p,f) + 1)) `2 by A2, A12, JORDAN5B:32, SPPOL_1:63; :: thesis: verum

end;

end;

end;

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

suppose p <> f . ((Index p,f) + 1) ; :: thesis: L_Cut f,p is special

then L_Cut f,p = <*p*> ^ (mid f,((Index p,f) + 1),(len f)) by JORDAN3:def 4;
hence L_Cut f,p is special by A3, A6, A7, A8, A11, A13, GOBOARD2:13; :: thesis: verum

end;

suppose p = f . ((Index p,f) + 1) ; :: thesis: L_Cut f,p is special

hence L_Cut f,p is special by A6, JORDAN3:def 4; :: thesis: verum

end;

end;