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 )
A2: mid (f,((Index (p,f)) + 1),(len f)) is special by A1, Th27;
A3: <*p*> /. 1 = p by FINSEQ_4:16;
assume A4: p in L~ f ; :: thesis: L_Cut (f,p) is special
then Index (p,f) < len f by JORDAN3:8;
then A5: (Index (p,f)) + 1 <= len f by NAT_1:13;
1 <= Index (p,f) by A4, JORDAN3:8;
then A6: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A5, TOPREAL1:def 3;
A7: now :: thesis: ( ( LSeg (f,(Index (p,f))) is vertical & p `1 = (f /. ((Index (p,f)) + 1)) `1 ) or ( LSeg (f,(Index (p,f))) is horizontal & p `2 = (f /. ((Index (p,f)) + 1)) `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)) `1
hence p `1 = (f /. ((Index (p,f)) + 1)) `1 by A4, A6, JORDAN5B:29, SPPOL_1:41; :: 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 A4, A6, JORDAN5B:29, SPPOL_1:40; :: thesis: verum
end;
end;
end;
A8: len <*p*> = 1 by FINSEQ_1:39;
len f <> 0 by A4, TOPREAL1:22;
then len f > 0 by NAT_1:3;
then len f >= 0 + 1 by NAT_1:13;
then A9: len f in dom f by FINSEQ_3:25;
(Index (p,f)) + 1 >= 1 by NAT_1:11;
then (Index (p,f)) + 1 in dom f by A5, FINSEQ_3:25;
then A10: (mid (f,((Index (p,f)) + 1),(len f))) /. 1 = f /. ((Index (p,f)) + 1) by A9, SPRECT_2:8;
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 3;
hence L_Cut (f,p) is special by A2, A8, A3, A10, A7, GOBOARD2:8; :: 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 A2, JORDAN3:def 3; :: thesis: verum
end;
end;