let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)
for n being Element of NAT st f is special & p in LSeg f,n holds
Ins f,n,p is special
let p be Point of (TOP-REAL 2); :: thesis: for n being Element of NAT st f is special & p in LSeg f,n holds
Ins f,n,p is special
let n be Element of NAT ; :: thesis: ( f is special & p in LSeg f,n implies Ins f,n,p is special )
assume that
A1: f is special and
A2: p in LSeg f,n ; :: thesis: Ins f,n,p is special
set f1 = f | n;
set g1 = (f | n) ^ <*p*>;
set f2 = f /^ n;
A3: ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = ((f | n) ^ <*p*>) /. ((len (f | n)) + 1) by FINSEQ_2:19
.= p by FINSEQ_4:82 ;
A4: ( 1 <= n & n + 1 <= len f ) by A2, TOPREAL1:def 5;
A5: n <= n + 1 by NAT_1:11;
then A6: n <= len f by A4, XXREAL_0:2;
A7: len (f | n) = n by A4, A5, FINSEQ_1:80, XXREAL_0:2;
then A8: n in dom (f | n) by A4, FINSEQ_3:27;
1 <= (len f) - n by A4, XREAL_1:21;
then 1 <= len (f /^ n) by A6, RFINSEQ:def 2;
then A9: 1 in dom (f /^ n) by FINSEQ_3:27;
A10: LSeg f,n = LSeg (f /. n),(f /. (n + 1)) by A4, TOPREAL1:def 5;
A11: f /. n = (f | n) /. (len (f | n)) by A7, A8, FINSEQ_4:85;
A12: f /. (n + 1) = (f /^ n) /. 1 by A9, FINSEQ_5:30;
A13: f | n is special by A1;
set p1 = (f | n) /. (len (f | n));
set p2 = (f /^ n) /. 1;
A14: ( ((f | n) /. (len (f | n))) `1 = ((f /^ n) /. 1) `1 or ((f | n) /. (len (f | n))) `2 = ((f /^ n) /. 1) `2 ) by A1, A4, A11, A12, TOPREAL1:def 7;
A15: (f | n) /. (len (f | n)) = |[(((f | n) /. (len (f | n))) `1 ),(((f | n) /. (len (f | n))) `2 )]| by EUCLID:57;
A16: (f /^ n) /. 1 = |[(((f /^ n) /. 1) `1 ),(((f /^ n) /. 1) `2 )]| by EUCLID:57;
<*p*> /. 1 = p by FINSEQ_4:25;
then A17: ( ((f | n) /. (len (f | n))) `1 = (<*p*> /. 1) `1 or ((f | n) /. (len (f | n))) `2 = (<*p*> /. 1) `2 ) by A2, A10, A11, A12, A14, A15, A16, TOPREAL3:17, TOPREAL3:18;
<*p*> is special by Th39;
then A18: (f | n) ^ <*p*> is special by A13, A17, Lm14;
set q1 = ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>));
A19: ( (((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))) `1 = ((f /^ n) /. 1) `1 or (((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))) `2 = ((f /^ n) /. 1) `2 ) by A2, A3, A10, A11, A12, A14, A15, A16, TOPREAL3:17, TOPREAL3:18;
f /^ n is special by A1;
then ((f | n) ^ <*p*>) ^ (f /^ n) is special by A18, A19, Lm14;
hence Ins f,n,p is special by FINSEQ_5:def 4; :: thesis: verum