let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)
for n being 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 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 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 7 :: 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 :: thesis: ( ( i = 0 & LSeg ((Ins (f,n,p)),i) = {} ) or ( j + 1 > len (Ins (f,n,p)) & LSeg ((Ins (f,n,p)),j) = {} ) )

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 3; :: 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 3; :: 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) ; :: 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:69;
A14: 1 <= n by A3, TOPREAL1:def 3;
A15: n + 1 <= len f by A3, TOPREAL1:def 3;
A16: len ((f | n) ^ <*p*>) = (len (f | n)) + 1 by FINSEQ_2:16;
then A17: ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = p by FINSEQ_4:67;
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:59, XXREAL_0:2;
(i + 1) + 1 <= j by A5, NAT_1:13;
then ((i + 1) + 1) + 1 <= j + 1 by XREAL_1:6;
then A21: ((i + 1) + 1) + 1 <= (len f) + 1 by A8, A13, XXREAL_0:2;
then (i + 1) + 1 <= len f by XREAL_1:6;
then A22: i + 1 <= len f by A12, XXREAL_0:2;

now :: thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)

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; :: 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 :: thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)

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:19;
then 1 <= len (f /^ n) by A19, RFINSEQ:def 1;
then 1 in dom (f /^ n) by FINSEQ_3:25;
then A29: f /. (n + 1) = (f /^ n) /. 1 by FINSEQ_5:27;
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:68;
Z1: n + 1 in dom f by A15, A28, FINSEQ_3:25;
Z2: (n + 1) + 1 >= 1 by NAT_1:11;
(n + 1) + 1 <= (len f) + 1 by A15, XREAL_1:6;
then (n + 1) + 1 <= len (Ins (f,n,p)) by A13;
then (n + 1) + 1 in dom (Ins (f,n,p)) by Z2, FINSEQ_3:25;
then A31: (Ins (f,n,p)) /. ((n + 1) + 1) = (Ins (f,n,p)) . ((n + 1) + 1) by PARTFUN1:def 6
.= f . (n + 1) by A15, FINSEQ_5:74
.= f /. (n + 1) by Z1, PARTFUN1:def 6 ;
A32: n in dom (f | n) by A14, A20, FINSEQ_3:25;
then A33: f /. n = (f | n) /. (len (f | n)) by A20, FINSEQ_4:70;
(n + 1) + 1 <= len (Ins (f,n,p)) by A13, A15, XREAL_1:6;
then A34: LSeg ((Ins (f,n,p)),(n + 1)) = LSeg (p,((f /^ n) /. 1)) by A17, A29, A31, A28, A30, TOPREAL1:def 3;
A35: (f | n) /. (len (f | n)) = ((f | n) ^ <*p*>) /. (len (f | n)) by A20, A32, FINSEQ_4:68;
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 3 ;
A37: LSeg (f,n) = LSeg ((f /. n),(f /. (n + 1))) by A14, A15, TOPREAL1:def 3;
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:5;
A39: (LSeg (((f | n) /. (len (f | n))),p)) /\ (LSeg (p,((f /^ n) /. 1))) = {p} by A3, A37, A33, A29, TOPREAL1:8;

now :: thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)

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 :: thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)

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;
(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;
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) ; :: 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 :: thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)

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 :: thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)

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:6;
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;
assume not LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; :: thesis: contradiction
then consider x being object 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:68;
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:134;
hence contradiction by A4, A53, PARTFUN2:2; :: 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;
(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;
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) ; :: 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:5;
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:19;
reconsider j9 = j - 1 as Element of NAT by A9, A11, INT_1:5, XXREAL_0:2;
A58: n + nj = j9 ;
(i + 1) + 1 <= n + 1 by A40, XREAL_1:6;
then (i + 1) + 1 < j by A56, XXREAL_0:2;
then A59: i + 1 < j9 by XREAL_1:20;
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; :: 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:5;
A61: (n + 1) + 1 <= j by A5, A60, NAT_1:13;
then A62: 1 <= nj by XREAL_1:19;
reconsider j9 = j - 1 as Element of NAT by A9, A11, INT_1:5, 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 :: thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)

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:20;
then A65: LSeg (f,i) misses LSeg (f,j9) by A2;
(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;
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) ; :: 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:6;
then A67: (LSeg (f,n)) /\ (LSeg (f,j9)) = {(f /. j9)} by A1, A14, A66;
assume not LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; :: thesis: contradiction
then consider x being object 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:68;
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:134;
hence contradiction by A4, A72, PARTFUN2:2; :: 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:5, 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:20;
then A75: LSeg (f,n) misses LSeg (f,j9) by A2;
n + 1 <= (n + 1) + 1 by NAT_1:11;
then reconsider nj = j - (n + 1) as Element of NAT by A5, A74, INT_1:5, XXREAL_0:2;
A76: 1 <= nj by A5, A74, XREAL_1:19;
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;
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; :: 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:5, 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:19;
reconsider ni = i - (n + 1) as Element of NAT by A78, INT_1:5;
(n + 1) + 1 <= i by A78, NAT_1:13;
then A80: 1 <= ni by XREAL_1:19;
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:9;
then A81: ni + 1 <= (len f) - n ;
reconsider i9 = i - 1 as Element of NAT by A7, INT_1:5, NAT_1:14;
reconsider j9 = j - 1 as Element of NAT by A9, A11, INT_1:5, XXREAL_0:2;
A82: n + ni = i9 ;
(i + 1) - 1 < j9 by A5, XREAL_1:9;
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; :: 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;