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.
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
set fp = Ins f,n,p;

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

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

now

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

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

j <= j + 1 by NAT_1:11;
then i < j + 1 by A11, XXREAL_0:2;
then i < n by A22, XXREAL_0:2;
then A23: i + 1 <= n by NAT_1:13;
then A24: LSeg (Ins f,n,p),i = LSeg ((f | n) ^ <*p*>),i by A9, A13, A16, A18, Th6, XXREAL_0:2
.= LSeg (f | n),i by A18, A23, Th6
.= LSeg f,i by A18, A23, Th3 ;
LSeg (Ins f,n,p),j = LSeg ((f | n) ^ <*p*>),j by A9, A13, A16, A18, A22, Th6, XXREAL_0:2
.= LSeg (f | n),j by A18, A22, Th6
.= LSeg f,j by A18, A22, 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 A25: n <= j by NAT_1:13;

now

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

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

A27: LSeg f,n = LSeg (f /. n),(f /. (n + 1)) by A15, TOPREAL1:def 5;
A28: n in dom (f | n) by A15, A18, FINSEQ_3:27;
then A29: f /. n = (f | n) /. (len (f | n)) by A18, FINSEQ_4:85;
1 <= (len f) - n by A15, XREAL_1:21;
then 1 <= len (f /^ n) by A17, RFINSEQ:def 2;
then 1 in dom (f /^ n) by FINSEQ_3:27;
then A30: f /. (n + 1) = (f /^ n) /. 1 by FINSEQ_5:30;
then A31: (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, A14, A27, A29, TOPREAL1:11;
A32: (f | n) /. (len (f | n)) = ((f | n) ^ <*p*>) /. (len (f | n)) by A18, A28, FINSEQ_4:83;
A33: LSeg (Ins f,n,p),n = LSeg ((f | n) ^ <*p*>),n by A9, A13, A18, Th6
.= LSeg ((f | n) /. (len (f | n))),p by A13, A14, A15, A18, A32, TOPREAL1:def 5 ;
A34: (Ins f,n,p) /. ((n + 1) + 1) = f /. (n + 1) by A15, FINSEQ_5:77;
A35: 1 <= n + 1 by NAT_1:11;
A36: (n + 1) + 1 <= len (Ins f,n,p) by A12, A15, XREAL_1:8;
len ((f | n) ^ <*p*>) in dom ((f | n) ^ <*p*>) by FINSEQ_5:6;
then (Ins f,n,p) /. (n + 1) = ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) by A9, A13, A18, FINSEQ_4:83;
then A37: LSeg (Ins f,n,p),(n + 1) = LSeg p,((f /^ n) /. 1) by A14, A30, A34, A35, A36, TOPREAL1:def 5;
A38: (LSeg ((f | n) /. (len (f | n))),p) /\ (LSeg p,((f /^ n) /. 1)) = {p} by A3, A27, A29, A30, 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 A39: i + 1 <= n by NAT_1:13;
then A40: LSeg (Ins f,n,p),i = LSeg ((f | n) ^ <*p*>),i by A9, A13, A16, A18, Th6, XXREAL_0:2
.= LSeg (f | n),i by A18, A39, Th6
.= LSeg f,i by A18, A39, Th3 ;

now

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

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

then A42: 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 A27, A29, A30, A31, A33, A40, A41, XBOOLE_1:7, XBOOLE_1:26;
then (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) c= {} by A42, 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 A25, XXREAL_0:1;
then A43: n + 1 <= j by NAT_1:13;

now

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

suppose A44: 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 A45: i + 1 = n ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then A46: LSeg (Ins f,n,p),i = LSeg ((f | n) ^ <*p*>),i by A9, A13, A18, Th6, NAT_1:11
.= LSeg (f | n),i by A18, A45, Th6
.= LSeg f,i by A18, A45, Th3 ;
i + (1 + 1) <= len f by A19, XREAL_1:8;
then A47: (LSeg (Ins f,n,p),i) /\ (LSeg f,n) = {(f /. n)} by A1, A10, A45, A46, 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
A48: x in (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) by XBOOLE_0:4;
A49: n in dom f by A15, GOBOARD2:3;
A50: x in LSeg (Ins f,n,p),i by A48, XBOOLE_0:def 4;
A51: x in LSeg (Ins f,n,p),j by A48, XBOOLE_0:def 4;
then x in LSeg f,n by A14, A27, A29, A30, A31, A37, A44, XBOOLE_0:def 3;
then x in {(f /. n)} by A47, A50, XBOOLE_0:def 4;
then A52: x = f /. n by TARSKI:def 1;
then x in LSeg (Ins f,n,p),n by A29, A33, RLTOPSP1:69;
then x in (LSeg (Ins f,n,p),n) /\ (LSeg (Ins f,n,p),(n + 1)) by A44, A51, XBOOLE_0:def 4;
then p = f /. n by A33, A37, A38, A52, TARSKI:def 1;
hence contradiction by A4, A49, 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 A39, XXREAL_0:1;
then A53: 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 A14, A27, A29, A30, A31, A37, A40, A44, XBOOLE_1:7, XBOOLE_1:26;
then (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) c= {} by A53, 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 j <> n + 1 ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then A54: n + 1 < j by A43, XXREAL_0:1;
then A55: (n + 1) + 1 <= j by NAT_1:13;
reconsider j' = j - 1 as Element of NAT by A10, A11, INT_1:18, XXREAL_0:2;
reconsider nj = j - (n + 1) as Element of NAT by A43, INT_1:18;
A56: j = nj + (n + 1) ;
A57: 1 <= nj by A55, XREAL_1:21;
A58: n + nj = j' ;
(i + 1) + 1 <= n + 1 by A39, XREAL_1:8;
then (i + 1) + 1 < j by A54, XXREAL_0:2;
then A59: i + 1 < j' by XREAL_1:22;
LSeg (Ins f,n,p),j = LSeg (f /^ n),nj by A9, A13, A18, A56, A57, Th7
.= LSeg f,j' by A17, A57, A58, Th4 ;
hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j by A2, A40, 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 A61: (n + 1) + 1 <= j by A5, NAT_1:13;
reconsider j' = j - 1 as Element of NAT by A10, A11, INT_1:18, XXREAL_0:2;
reconsider nj = j - (n + 1) as Element of NAT by A5, A60, INT_1:18;
A62: j = nj + (n + 1) ;
A63: 1 <= nj by A61, XREAL_1:21;
A64: n + nj = j' ;
A65: LSeg (Ins f,n,p),j = LSeg (f /^ n),nj by A9, A13, A18, A62, A63, Th7
.= LSeg f,j' by A17, A63, A64, 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 < j' by A60, XREAL_1:22;
then A66: LSeg f,i misses LSeg f,j' by A2, TOPREAL1:def 9;
(LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) c= (LSeg f,i) /\ (LSeg f,j') by A27, A29, A30, A31, A33, A60, A65, XBOOLE_1:7, XBOOLE_1:26;
then (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) c= {} by A66, 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 A67: 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, A12, XREAL_1:8;
then A68: (LSeg f,n) /\ (LSeg f,j') = {(f /. j')} by A1, A15, A67, 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
A69: x in (LSeg (Ins f,n,p),i) /\ (LSeg (Ins f,n,p),j) by XBOOLE_0:4;
A70: n + 1 in dom f by A15, GOBOARD2:3;
A71: x in LSeg (Ins f,n,p),j by A69, XBOOLE_0:def 4;
A72: x in LSeg (Ins f,n,p),i by A69, XBOOLE_0:def 4;
then x in LSeg f,n by A27, A29, A30, A31, A33, A60, XBOOLE_0:def 3;
then x in {(f /. (n + 1))} by A65, A67, A68, A71, XBOOLE_0:def 4;
then A73: x = f /. (n + 1) by TARSKI:def 1;
then x in LSeg (Ins f,n,p),(n + 1) by A30, A37, RLTOPSP1:69;
then x in (LSeg (Ins f,n,p),n) /\ (LSeg (Ins f,n,p),(n + 1)) by A60, A72, XBOOLE_0:def 4;
then p = f /. (n + 1) by A33, A37, A38, A73, TARSKI:def 1;
hence contradiction by A4, A70, 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 i > n ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then i >= n + 1 by NAT_1:13;
then A74: i = n + 1 by A26, XXREAL_0:1;
reconsider j' = j - 1 as Element of NAT by A10, A11, INT_1:18, XXREAL_0:2;
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;
A75: j = nj + (n + 1) ;
A76: 1 <= nj by A5, A74, XREAL_1:21;
A77: n + nj = j' ;
A78: LSeg (Ins f,n,p),j = LSeg (f /^ n),nj by A9, A13, A18, A75, A76, Th7
.= LSeg f,j' by A17, A76, A77, Th4 ;
n + 1 < j' by A5, A74, XREAL_1:22;
then A79: LSeg f,n misses LSeg f,j' by A2, TOPREAL1:def 9;
(LSeg (Ins f,n,p),(n + 1)) /\ (LSeg (Ins f,n,p),j) c= (LSeg f,n) /\ (LSeg f,j') by A14, A27, A29, A30, A31, A37, A78, XBOOLE_1:7, XBOOLE_1:26;
then (LSeg (Ins f,n,p),(n + 1)) /\ (LSeg (Ins f,n,p),j) c= {} by A79, 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 A80: i > n + 1 ; :: thesis: LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j

then A81: (n + 1) + 1 <= i by NAT_1:13;
reconsider ni = i - (n + 1) as Element of NAT by A80, INT_1:18;
A82: i = ni + (n + 1) ;
reconsider i' = i - 1 as Element of NAT by A7, INT_1:18, NAT_1:14;
A83: 1 <= ni by A81, XREAL_1:21;
len f <= (len f) + 1 by NAT_1:11;
then i + 1 <= (len f) + 1 by A21, XXREAL_0:2;
then (i + 1) - (n + 1) <= ((len f) + 1) - (n + 1) by XREAL_1:11;
then A84: ni + 1 <= (len f) - n ;
A85: n + ni = i' ;
A86: LSeg (Ins f,n,p),i = LSeg (f /^ n),ni by A9, A13, A18, A82, A83, Th7
.= LSeg f,i' by A83, A84, A85, Th5 ;
reconsider j' = j - 1 as Element of NAT by A10, A11, INT_1:18, XXREAL_0:2;
A87: n + 1 < j by A11, A80, XXREAL_0:2;
reconsider nj = j - (n + 1) as Element of NAT by A11, A80, INT_1:18, XXREAL_0:2;
A88: j = nj + (n + 1) ;
(n + 1) + 1 <= j by A87, NAT_1:13;
then A89: 1 <= nj by XREAL_1:21;
A90: n + nj = j' ;
(i + 1) - 1 < j' by A5, XREAL_1:11;
then A91: i' + 1 < j' ;
LSeg (Ins f,n,p),j = LSeg (f /^ n),nj by A9, A13, A18, A88, A89, Th7
.= LSeg f,j' by A17, A89, A90, Th4 ;
hence LSeg (Ins f,n,p),i misses LSeg (Ins f,n,p),j by A2, A86, A91, 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;