let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)

for n being 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 Nat st f is special & p in LSeg (f,n) holds

Ins (f,n,p) is special

let n be 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

A3: n + 1 <= len f by A2, TOPREAL1:def 3;

then A4: 1 <= (len f) - n by XREAL_1:19;

A5: 1 <= n by A2, TOPREAL1:def 3;

then A6: LSeg (f,n) = LSeg ((f /. n),(f /. (n + 1))) by A3, TOPREAL1:def 3;

set f1 = f | n;

set g1 = (f | n) ^ <*p*>;

set f2 = f /^ n;

set p1 = (f | n) /. (len (f | n));

set p2 = (f /^ n) /. 1;

A7: (f | n) /. (len (f | n)) = |[(((f | n) /. (len (f | n))) `1),(((f | n) /. (len (f | n))) `2)]| by EUCLID:53;

A8: n <= n + 1 by NAT_1:11;

then n <= len f by A3, XXREAL_0:2;

then 1 <= len (f /^ n) by A4, RFINSEQ:def 1;

then 1 in dom (f /^ n) by FINSEQ_3:25;

then A9: f /. (n + 1) = (f /^ n) /. 1 by FINSEQ_5:27;

A10: len (f | n) = n by A3, A8, FINSEQ_1:59, XXREAL_0:2;

then n in dom (f | n) by A5, FINSEQ_3:25;

then A11: f /. n = (f | n) /. (len (f | n)) by A10, FINSEQ_4:70;

then A12: ( ((f | n) /. (len (f | n))) `1 = ((f /^ n) /. 1) `1 or ((f | n) /. (len (f | n))) `2 = ((f /^ n) /. 1) `2 ) by A1, A5, A3, A9;

set q1 = ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>));

A13: (f /^ n) /. 1 = |[(((f /^ n) /. 1) `1),(((f /^ n) /. 1) `2)]| by EUCLID:53;

<*p*> /. 1 = p by FINSEQ_4:16;

then ( ((f | n) /. (len (f | n))) `1 = (<*p*> /. 1) `1 or ((f | n) /. (len (f | n))) `2 = (<*p*> /. 1) `2 ) by A2, A6, A11, A9, A12, A7, A13, TOPREAL3:11, TOPREAL3:12;

then A14: (f | n) ^ <*p*> is special by A1, Lm13;

((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = ((f | n) ^ <*p*>) /. ((len (f | n)) + 1) by FINSEQ_2:16

.= p by FINSEQ_4:67 ;

then ( (((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, A6, A11, A9, A12, A7, A13, TOPREAL3:11, TOPREAL3:12;

then ((f | n) ^ <*p*>) ^ (f /^ n) is special by A1, A14, Lm13;

hence Ins (f,n,p) is special by FINSEQ_5:def 4; :: thesis: verum

for n being 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 Nat st f is special & p in LSeg (f,n) holds

Ins (f,n,p) is special

let n be 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

A3: n + 1 <= len f by A2, TOPREAL1:def 3;

then A4: 1 <= (len f) - n by XREAL_1:19;

A5: 1 <= n by A2, TOPREAL1:def 3;

then A6: LSeg (f,n) = LSeg ((f /. n),(f /. (n + 1))) by A3, TOPREAL1:def 3;

set f1 = f | n;

set g1 = (f | n) ^ <*p*>;

set f2 = f /^ n;

set p1 = (f | n) /. (len (f | n));

set p2 = (f /^ n) /. 1;

A7: (f | n) /. (len (f | n)) = |[(((f | n) /. (len (f | n))) `1),(((f | n) /. (len (f | n))) `2)]| by EUCLID:53;

A8: n <= n + 1 by NAT_1:11;

then n <= len f by A3, XXREAL_0:2;

then 1 <= len (f /^ n) by A4, RFINSEQ:def 1;

then 1 in dom (f /^ n) by FINSEQ_3:25;

then A9: f /. (n + 1) = (f /^ n) /. 1 by FINSEQ_5:27;

A10: len (f | n) = n by A3, A8, FINSEQ_1:59, XXREAL_0:2;

then n in dom (f | n) by A5, FINSEQ_3:25;

then A11: f /. n = (f | n) /. (len (f | n)) by A10, FINSEQ_4:70;

then A12: ( ((f | n) /. (len (f | n))) `1 = ((f /^ n) /. 1) `1 or ((f | n) /. (len (f | n))) `2 = ((f /^ n) /. 1) `2 ) by A1, A5, A3, A9;

set q1 = ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>));

A13: (f /^ n) /. 1 = |[(((f /^ n) /. 1) `1),(((f /^ n) /. 1) `2)]| by EUCLID:53;

<*p*> /. 1 = p by FINSEQ_4:16;

then ( ((f | n) /. (len (f | n))) `1 = (<*p*> /. 1) `1 or ((f | n) /. (len (f | n))) `2 = (<*p*> /. 1) `2 ) by A2, A6, A11, A9, A12, A7, A13, TOPREAL3:11, TOPREAL3:12;

then A14: (f | n) ^ <*p*> is special by A1, Lm13;

((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = ((f | n) ^ <*p*>) /. ((len (f | n)) + 1) by FINSEQ_2:16

.= p by FINSEQ_4:67 ;

then ( (((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, A6, A11, A9, A12, A7, A13, TOPREAL3:11, TOPREAL3:12;

then ((f | n) ^ <*p*>) ^ (f /^ n) is special by A1, A14, Lm13;

hence Ins (f,n,p) is special by FINSEQ_5:def 4; :: thesis: verum