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)

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)) ) )
;

end;

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)

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

end;

now :: thesis: ( ( i = 0 & LSeg ((Ins (f,n,p)),i) = {} ) or ( j + 1 > len (Ins (f,n,p)) & LSeg ((Ins (f,n,p)),j) = {} ) )

then
(LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) = {}
;end;

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

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)

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;

end;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)end;

hence
LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
; :: thesis: verumper cases
( j + 1 <= n or j + 1 > n )
;

end;

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;.= 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

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;

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

hence
LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
; :: thesis: verumper cases
( i <= n + 1 or i > n + 1 )
;

end;

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;

end;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)end;

hence
LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
; :: thesis: verumper cases
( i < n or i = n or i > n )
by XXREAL_0:1;

end;

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 ;

end;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)end;

hence
LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
; :: thesis: verumper cases
( j = n or j <> n )
;

end;

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;(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

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;

end;then A44: n + 1 <= j by NAT_1:13;

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

hence
LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
; :: thesis: verumper cases
( j = n + 1 or j <> n + 1 )
;

end;

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

end;

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

hence
LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
; :: thesis: verumper cases
( i + 1 = n or i + 1 <> n )
;

end;

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;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

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;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

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;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

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 ;

end;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)end;

hence
LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j)
; :: thesis: verumper cases
( j <> (n + 1) + 1 or j = (n + 1) + 1 )
;

end;

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;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

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;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

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;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

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;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