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 unfolded & f is s.n.c. & p in LSeg f,n & not p in rng f holds
Ins f,n,p is s.n.c.
let p be Point of (TOP-REAL 2); :: thesis: for n being Element of NAT st f is unfolded & f is s.n.c. & p in LSeg f,n & not p in rng f holds
Ins f,n,p is s.n.c.
let n be Element of NAT ; :: thesis: ( f is unfolded & f is s.n.c. & p in LSeg f,n & not p in rng f implies Ins f,n,p is s.n.c. )
assume that
A1: f is unfolded and
A2: f is s.n.c. and
A3: p in LSeg f,n and
A4: not p in rng f ; :: thesis: Ins f,n,p is s.n.c.
set fp = Ins f,n,p;
let i, j be Nat; :: according to TOPREAL1:def 9 :: thesis: ( j <= i + 1 or LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j )
assume A5: i + 1 < j ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

per cases ( i = 0 or j + 1 > len (Ins f,n,p) or ( i <> 0 & j + 1 <= len (Ins f,n,p) ) ) ;

suppose A6: ( i = 0 or j + 1 > len (Ins f,n,p) ) ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

now

per cases ( i = 0 or j + 1 > len (Ins f,n,p) ) by A6;

case i = 0 ; :: thesis: LSeg (Ins f,n,p),i = {}

hence LSeg (Ins f,n,p),i = {} by TOPREAL1:def 5; :: thesis: verum

end;

case j + 1 > len (Ins f,n,p) ; :: thesis: LSeg (Ins f,n,p),j = {}

hence LSeg (Ins f,n,p),j = {} by TOPREAL1:def 5; :: thesis: verum

end;

end;

end;

then (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) = {} ;
hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j by XBOOLE_0:def 7; :: thesis: verum

end;

suppose that A7: i <> 0 and
A8: j + 1 <= len (Ins f,n,p) ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

A9: 1 <= i by A7, NAT_1:14;
set f1 = f | n;
set g1 = (f | n) ^ <*p*>;
set f2 = f /^ n;
A10: Ins f,n,p = ((f | n) ^ <*p*>) ^ (f /^ n) by FINSEQ_5:def 4;
i <= i + 1 by NAT_1:11;
then A11: i < j by A5, XXREAL_0:2;
A12: i + 1 <= (i + 1) + 1 by NAT_1:11;
A13: len (Ins f,n,p) = (len f) + 1 by FINSEQ_5:72;
A14: 1 <= n by A3, TOPREAL1:def 5;
A15: n + 1 <= len f by A3, TOPREAL1:def 5;
A16: len ((f | n) ^ <*p*>) = (len (f | n)) + 1 by FINSEQ_2:19;
then A17: ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = p by FINSEQ_4:82;
A18: n <= n + 1 by NAT_1:11;
then A19: n <= len f by A15, XXREAL_0:2;
A20: len (f | n) = n by A15, A18, FINSEQ_1:80, XXREAL_0:2;
(i + 1) + 1 <= j by A5, NAT_1:13;
then ((i + 1) + 1) + 1 <= j + 1 by XREAL_1:8;
then A21: ((i + 1) + 1) + 1 <= (len f) + 1 by A8, A13, XXREAL_0:2;
then (i + 1) + 1 <= len f by XREAL_1:8;
then A22: i + 1 <= len f by A12, XXREAL_0:2;

now

per cases ( j + 1 <= n or j + 1 > n ) ;

suppose A23: j + 1 <= n ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then A24: LSeg (Ins f,n,p),j = LSeg ((f | n) ^ <*p*>),j by A10, A16, A18, A20, Th6, XXREAL_0:2
.= LSeg (f | n),j by A20, A23, Th6
.= LSeg f,j by A20, A23, Th3 ;
j <= j + 1 by NAT_1:11;
then i < j + 1 by A11, XXREAL_0:2;
then i < n by A23, XXREAL_0:2;
then A25: i + 1 <= n by NAT_1:13;
then LSeg (Ins f,n,p),i = LSeg ((f | n) ^ <*p*>),i by A10, A16, A18, A20, Th6, XXREAL_0:2
.= LSeg (f | n),i by A20, A25, Th6
.= LSeg f,i by A20, A25, Th3 ;
hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j by A2, A5, A24, TOPREAL1:def 9; :: thesis: verum

end;

suppose j + 1 > n ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then A26: n <= j by NAT_1:13;

now

per cases ( i <= n + 1 or i > n + 1 ) ;

suppose A27: i <= n + 1 ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

A28: 1 <= n + 1 by NAT_1:11;
1 <= (len f) - n by A15, XREAL_1:21;
then 1 <= len (f /^ n) by A19, RFINSEQ:def 2;
then 1 in dom (f /^ n) by FINSEQ_3:27;
then A29: f /. (n + 1) = (f /^ n) /. 1 by FINSEQ_5:30;
len ((f | n) ^ <*p*>) in dom ((f | n) ^ <*p*>) by FINSEQ_5:6;
then A30: (Ins f,n,p) /. (n + 1) = ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) by A10, A16, A20, FINSEQ_4:83;
A31: (Ins f,n,p) /. ((n + 1) + 1) = f /. (n + 1) by A15, FINSEQ_5:77;
A32: n in dom (f | n) by A14, A20, FINSEQ_3:27;
then A33: f /. n = (f | n) /. (len (f | n)) by A20, FINSEQ_4:85;
(n + 1) + 1 <= len (Ins f,n,p) by A13, A15, XREAL_1:8;
then A34: LSeg (Ins f,n,p),(n + 1) = LSeg p,((f /^ n) /. 1) by A17, A29, A31, A28, A30, TOPREAL1:def 5;
A35: (f | n) /. (len (f | n)) = ((f | n) ^ <*p*>) /. (len (f | n)) by A20, A32, FINSEQ_4:83;
A36: LSeg (Ins f,n,p),n = LSeg ((f | n) ^ <*p*>),n by A10, A16, A20, Th6
.= LSeg ((f | n) /. (len (f | n))),p by A16, A17, A14, A20, A35, TOPREAL1:def 5 ;
A37: LSeg f,n = LSeg (f /. n),(f /. (n + 1)) by A14, A15, TOPREAL1:def 5;
then A38: (LSeg ((f | n) /. (len (f | n))),p) \/ (LSeg (((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)) = LSeg ((f | n) /. (len (f | n))),((f /^ n) /. 1) by A3, A17, A33, A29, TOPREAL1:11;
A39: (LSeg ((f | n) /. (len (f | n))),p) /\ (LSeg p,((f /^ n) /. 1)) = {p} by A3, A37, A33, A29, TOPREAL1:14;

now

per cases ( i < n or i = n or i > n ) by XXREAL_0:1;

suppose i < n ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then A40: i + 1 <= n by NAT_1:13;
then A41: LSeg (Ins f,n,p),i = LSeg ((f | n) ^ <*p*>),i by A10, A16, A18, A20, Th6, XXREAL_0:2
.= LSeg (f | n),i by A20, A40, Th6
.= LSeg f,i by A20, A40, Th3 ;

now

per cases ( j = n or j <> n ) ;

suppose A42: j = n ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then A43: LSeg f,i misses LSeg f,n by A2, A5, TOPREAL1:def 9;
(LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) c= (LSeg f,i) /\ (LSeg f,n) by A37, A33, A29, A38, A36, A41, A42, XBOOLE_1:7, XBOOLE_1:26;
then (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) c= {} by A43, XBOOLE_0:def 7;
then (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) = {} by XBOOLE_1:3;
hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j by XBOOLE_0:def 7; :: thesis: verum

end;

suppose j <> n ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then n < j by A26, XXREAL_0:1;
then A44: n + 1 <= j by NAT_1:13;

now

per cases ( j = n + 1 or j <> n + 1 ) ;

suppose A45: j = n + 1 ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

now

per cases ( i + 1 = n or i + 1 <> n ) ;

suppose A46: i + 1 = n ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

A47: i + (1 + 1) <= len f by A21, XREAL_1:8;
LSeg (Ins f,n,p),i = LSeg ((f | n) ^ <*p*>),i by A10, A16, A20, A46, Th6, NAT_1:11
.= LSeg (f | n),i by A20, A46, Th6
.= LSeg f,i by A20, A46, Th3 ;
then A48: (LSeg (Ins f,n,p),i) /\ (LSeg f,n) = {(f /. n)} by A1, A9, A46, A47, TOPREAL1:def 8;
assume not LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j ; :: thesis: contradiction
then consider x being set such that
A49: x in (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) by XBOOLE_0:4;
A50: x in LSeg (Ins f,n,p),i by A49, XBOOLE_0:def 4;
A51: x in LSeg (Ins f,n,p),j by A49, XBOOLE_0:def 4;
then x in LSeg f,n by A17, A37, A33, A29, A38, A34, A45, XBOOLE_0:def 3;
then x in {(f /. n)} by A48, A50, XBOOLE_0:def 4;
then A52: x = f /. n by TARSKI:def 1;
then x in LSeg (Ins f,n,p),n by A33, A36, RLTOPSP1:69;
then x in (LSeg (Ins f,n,p),n) /\ (LSeg (Ins f,n,p),(n + 1)) by A45, A51, XBOOLE_0:def 4;
then A53: p = f /. n by A36, A34, A39, A52, TARSKI:def 1;
n in dom f by A14, A15, SEQ_4:151;
hence contradiction by A4, A53, PARTFUN2:4; :: thesis: verum

end;

suppose i + 1 <> n ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then i + 1 < n by A40, XXREAL_0:1;
then A54: LSeg f,i misses LSeg f,n by A2, TOPREAL1:def 9;
(LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) c= (LSeg f,i) /\ (LSeg f,n) by A17, A37, A33, A29, A38, A34, A41, A45, XBOOLE_1:7, XBOOLE_1:26;
then (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) c= {} by A54, XBOOLE_0:def 7;
then (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) = {} by XBOOLE_1:3;
hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j by XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j ; :: thesis: verum

end;

suppose A55: j <> n + 1 ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

reconsider nj = j - (n + 1) as Element of NAT by A44, INT_1:18;
A56: n + 1 < j by A44, A55, XXREAL_0:1;
then (n + 1) + 1 <= j by NAT_1:13;
then A57: 1 <= nj by XREAL_1:21;
reconsider j9 = j - 1 as Element of NAT by A9, A11, INT_1:18, XXREAL_0:2;
A58: n + nj = j9 ;
(i + 1) + 1 <= n + 1 by A40, XREAL_1:8;
then (i + 1) + 1 < j by A56, XXREAL_0:2;
then A59: i + 1 < j9 by XREAL_1:22;
j = nj + (n + 1) ;
then LSeg (Ins f,n,p),j = LSeg (f /^ n),nj by A10, A16, A20, A57, Th7
.= LSeg f,j9 by A19, A57, A58, Th4 ;
hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j by A2, A41, A59, TOPREAL1:def 9; :: thesis: verum

end;

end;

end;

hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j ; :: thesis: verum

end;

end;

end;

hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j ; :: thesis: verum

end;

suppose A60: i = n ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then reconsider nj = j - (n + 1) as Element of NAT by A5, INT_1:18;
A61: (n + 1) + 1 <= j by A5, A60, NAT_1:13;
then A62: 1 <= nj by XREAL_1:21;
reconsider j9 = j - 1 as Element of NAT by A9, A11, INT_1:18, XXREAL_0:2;
A63: n + nj = j9 ;
j = nj + (n + 1) ;
then A64: LSeg (Ins f,n,p),j = LSeg (f /^ n),nj by A10, A16, A20, A62, Th7
.= LSeg f,j9 by A19, A62, A63, Th4 ;

now

per cases ( j <> (n + 1) + 1 or j = (n + 1) + 1 ) ;

suppose j <> (n + 1) + 1 ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then (n + 1) + 1 < j by A61, XXREAL_0:1;
then i + 1 < j9 by A60, XREAL_1:22;
then A65: LSeg f,i misses LSeg f,j9 by A2, TOPREAL1:def 9;
(LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) c= (LSeg f,i) /\ (LSeg f,j9) by A37, A33, A29, A38, A36, A60, A64, XBOOLE_1:7, XBOOLE_1:26;
then (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) c= {} by A65, XBOOLE_0:def 7;
then (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) = {} by XBOOLE_1:3;
hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j by XBOOLE_0:def 7; :: thesis: verum

end;

suppose A66: j = (n + 1) + 1 ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then n + (1 + 1) <= len f by A8, A13, XREAL_1:8;
then A67: (LSeg f,n) /\ (LSeg f,j9) = {(f /. j9)} by A1, A14, A66, TOPREAL1:def 8;
assume not LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j ; :: thesis: contradiction
then consider x being set such that
A68: x in (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) by XBOOLE_0:4;
A69: x in LSeg (Ins f,n,p),j by A68, XBOOLE_0:def 4;
A70: x in LSeg (Ins f,n,p),i by A68, XBOOLE_0:def 4;
then x in LSeg f,n by A37, A33, A29, A38, A36, A60, XBOOLE_0:def 3;
then x in {(f /. (n + 1))} by A64, A66, A67, A69, XBOOLE_0:def 4;
then A71: x = f /. (n + 1) by TARSKI:def 1;
then x in LSeg (Ins f,n,p),(n + 1) by A29, A34, RLTOPSP1:69;
then x in (LSeg (Ins f,n,p),n) /\ (LSeg (Ins f,n,p),(n + 1)) by A60, A70, XBOOLE_0:def 4;
then A72: p = f /. (n + 1) by A36, A34, A39, A71, TARSKI:def 1;
n + 1 in dom f by A14, A15, SEQ_4:151;
hence contradiction by A4, A72, PARTFUN2:4; :: thesis: verum

end;

end;

end;

hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j ; :: thesis: verum

end;

suppose A73: i > n ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

reconsider j9 = j - 1 as Element of NAT by A9, A11, INT_1:18, XXREAL_0:2;
i >= n + 1 by A73, NAT_1:13;
then A74: i = n + 1 by A27, XXREAL_0:1;
then n + 1 < j9 by A5, XREAL_1:22;
then A75: LSeg f,n misses LSeg f,j9 by A2, TOPREAL1:def 9;
n + 1 <= (n + 1) + 1 by NAT_1:11;
then reconsider nj = j - (n + 1) as Element of NAT by A5, A74, INT_1:18, XXREAL_0:2;
A76: 1 <= nj by A5, A74, XREAL_1:21;
A77: n + nj = j9 ;
j = nj + (n + 1) ;
then LSeg (Ins f,n,p),j = LSeg (f /^ n),nj by A10, A16, A20, A76, Th7
.= LSeg f,j9 by A19, A76, A77, Th4 ;
then (LSeg (Ins f,n,p),(n + 1)) /\ (LSeg (Ins f,n,p),j) c= (LSeg f,n) /\ (LSeg f,j9) by A17, A37, A33, A29, A38, A34, XBOOLE_1:7, XBOOLE_1:26;
then (LSeg (Ins f,n,p),(n + 1)) /\ (LSeg (Ins f,n,p),j) c= {} by A75, XBOOLE_0:def 7;
then (LSeg (Ins f,n,p),(n + 1)) /\ (LSeg (Ins f,n,p),j) = {} by XBOOLE_1:3;
hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j by A74, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j ; :: thesis: verum

end;

suppose A78: i > n + 1 ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then reconsider nj = j - (n + 1) as Element of NAT by A11, INT_1:18, XXREAL_0:2;
n + 1 < j by A11, A78, XXREAL_0:2;
then (n + 1) + 1 <= j by NAT_1:13;
then A79: 1 <= nj by XREAL_1:21;
reconsider ni = i - (n + 1) as Element of NAT by A78, INT_1:18;
(n + 1) + 1 <= i by A78, NAT_1:13;
then A80: 1 <= ni by XREAL_1:21;
len f <= (len f) + 1 by NAT_1:11;
then i + 1 <= (len f) + 1 by A22, XXREAL_0:2;
then (i + 1) - (n + 1) <= ((len f) + 1) - (n + 1) by XREAL_1:11;
then A81: ni + 1 <= (len f) - n ;
reconsider i9 = i - 1 as Element of NAT by A7, INT_1:18, NAT_1:14;
reconsider j9 = j - 1 as Element of NAT by A9, A11, INT_1:18, XXREAL_0:2;
A82: n + ni = i9 ;
(i + 1) - 1 < j9 by A5, XREAL_1:11;
then A83: i9 + 1 < j9 ;
A84: n + nj = j9 ;
j = nj + (n + 1) ;
then A85: LSeg (Ins f,n,p),j = LSeg (f /^ n),nj by A10, A16, A20, A79, Th7
.= LSeg f,j9 by A19, A79, A84, Th4 ;
i = ni + (n + 1) ;
then LSeg (Ins f,n,p),i = LSeg (f /^ n),ni by A10, A16, A20, A80, Th7
.= LSeg f,i9 by A80, A81, A82, Th5 ;
hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j by A2, A83, A85, TOPREAL1:def 9; :: thesis: verum

end;

end;

end;

hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j ; :: thesis: verum

end;

end;

end;

hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j ; :: thesis: verum

end;

end;