let f, g be FinSequence of (TOP-REAL 2); ( f is s.n.c. & g is s.n.c. & L~ f misses L~ g & ( for i being Nat st 1 <= i & i + 2 <= len f holds
LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) ) & ( for i being Nat st 2 <= i & i + 1 <= len g holds
LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) ) implies f ^ g is s.n.c. )
assume that
A1:
f is s.n.c.
and
A2:
g is s.n.c.
and
A3:
(L~ f) /\ (L~ g) = {}
and
A4:
for i being Nat st 1 <= i & i + 2 <= len f holds
LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1))
and
A5:
for i being Nat st 2 <= i & i + 1 <= len g holds
LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1))
; XBOOLE_0:def 7 f ^ g is s.n.c.
let i, j be Nat; TOPREAL1:def 7 ( j <= i + 1 or LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) )
assume A6:
i + 1 < j
; LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
per cases
( i = 0 or j + 1 > len (f ^ g) or ( i <> 0 & j + 1 <= len (f ^ g) ) )
;
suppose that A8:
i <> 0
and A9:
j + 1
<= len (f ^ g)
;
LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)A10:
len (f ^ g) = (len f) + (len g)
by FINSEQ_1:22;
i <= i + 1
by NAT_1:11;
then A11:
i < j
by A6, XXREAL_0:2;
A12:
1
<= i
by A8, NAT_1:14;
now LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)per cases
( j + 1 <= len f or j + 1 > len f )
;
suppose A13:
j + 1
<= len f
;
LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
j <= j + 1
by NAT_1:11;
then
i < j + 1
by A11, XXREAL_0:2;
then
i < len f
by A13, XXREAL_0:2;
then
i + 1
<= len f
by NAT_1:13;
then A14:
LSeg (
(f ^ g),
i)
= LSeg (
f,
i)
by Th6;
LSeg (
(f ^ g),
j)
= LSeg (
f,
j)
by A13, Th6;
hence
LSeg (
(f ^ g),
i)
misses LSeg (
(f ^ g),
j)
by A1, A6, A14;
verum end; suppose
j + 1
> len f
;
LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)then A15:
len f <= j
by NAT_1:13;
then reconsider j9 =
j - (len f) as
Element of
NAT by INT_1:5;
(j + 1) - (len f) <= len g
by A9, A10, XREAL_1:20;
then A16:
j9 + 1
<= len g
;
A17:
(len f) + j9 = j
;
now LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)per cases
( i <= len f or i > len f )
;
suppose A18:
i <= len f
;
LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)then A19:
not
f is
empty
by A12;
now LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)per cases
( i = len f or i <> len f )
;
suppose A20:
i = len f
;
LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
not
g is
empty
by A16;
then A21:
LSeg (
(f ^ g),
i)
= LSeg (
(f /. (len f)),
(g /. 1))
by A19, A20, Th8;
((len f) + 1) + 1
<= j
by A6, A20, NAT_1:13;
then
(len f) + (1 + 1) <= j
;
then A22:
1
+ 1
<= j9
by XREAL_1:19;
then
LSeg (
(f ^ g),
j)
= LSeg (
g,
j9)
by A17, Th7, XXREAL_0:2;
hence
LSeg (
(f ^ g),
i)
misses LSeg (
(f ^ g),
j)
by A5, A16, A22, A21;
verum end; suppose
i <> len f
;
LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)then
i < len f
by A18, XXREAL_0:1;
then
i + 1
<= len f
by NAT_1:13;
then A23:
LSeg (
(f ^ g),
i)
= LSeg (
f,
i)
by Th6;
now LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)per cases
( j = len f or j <> len f )
;
suppose A24:
j = len f
;
LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)then
(i + 1) + 1
<= len f
by A6, NAT_1:13;
then A25:
i + (1 + 1) <= len f
;
not
g is
empty
by A9, A10, A24, XREAL_1:6;
then A26:
LSeg (
(f ^ g),
j)
= LSeg (
(f /. (len f)),
(g /. 1))
by A19, A24, Th8;
thus
LSeg (
(f ^ g),
i)
misses LSeg (
(f ^ g),
j)
by A4, A8, A23, A25, A26, NAT_1:14;
verum end; suppose
j <> len f
;
LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)then
len f < j
by A15, XXREAL_0:1;
then
(len f) + 1
<= j
by NAT_1:13;
then
1
<= j9
by XREAL_1:19;
then
LSeg (
(f ^ g),
((len f) + j9))
= LSeg (
g,
j9)
by Th7;
then A27:
LSeg (
(f ^ g),
j)
c= L~ g
by TOPREAL3:19;
LSeg (
(f ^ g),
i)
c= L~ f
by A23, TOPREAL3:19;
then
(LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) = {}
by A3, A27, XBOOLE_1:3, XBOOLE_1:27;
hence
LSeg (
(f ^ g),
i)
misses LSeg (
(f ^ g),
j)
;
verum end; end; end; hence
LSeg (
(f ^ g),
i)
misses LSeg (
(f ^ g),
j)
;
verum end; end; end; hence
LSeg (
(f ^ g),
i)
misses LSeg (
(f ^ g),
j)
;
verum end; suppose A28:
i > len f
;
LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)then
j <> len f
by A6, NAT_1:13;
then
len f < j
by A15, XXREAL_0:1;
then
(len f) + 1
<= j
by NAT_1:13;
then
1
<= j9
by XREAL_1:19;
then A29:
LSeg (
(f ^ g),
((len f) + j9))
= LSeg (
g,
j9)
by Th7;
reconsider i9 =
i - (len f) as
Element of
NAT by A28, INT_1:5;
(len f) + 1
<= i
by A28, NAT_1:13;
then
1
<= i9
by XREAL_1:19;
then A30:
LSeg (
(f ^ g),
((len f) + i9))
= LSeg (
g,
i9)
by Th7;
(i + 1) - (len f) < j9
by A6, XREAL_1:9;
then
i9 + 1
< j9
;
hence
LSeg (
(f ^ g),
i)
misses LSeg (
(f ^ g),
j)
by A2, A30, A29;
verum end; end; end; hence
LSeg (
(f ^ g),
i)
misses LSeg (
(f ^ g),
j)
;
verum end; end; end; hence
LSeg (
(f ^ g),
i)
misses LSeg (
(f ^ g),
j)
;
verum end; end;