let i, j be Nat; for f being FinSequence of (TOP-REAL 2) st 1 <= i & i <= j & j <= len f holds
L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }
let f be FinSequence of (TOP-REAL 2); ( 1 <= i & i <= j & j <= len f implies L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } )
assume that
A1:
1 <= i
and
A2:
i <= j
and
A3:
j <= len f
; L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }
set A = { (LSeg ((mid (f,i,j)),m)) where m is Nat : ( 1 <= m & m + 1 <= len (mid (f,i,j)) ) } ;
set B = { (LSeg (f,l)) where l is Nat : ( i <= l & l < j ) } ;
per cases
( i = j or i < j )
by A2, XXREAL_0:1;
suppose A4:
i = j
;
L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } A5:
{ (LSeg (f,l)) where l is Nat : ( i <= l & l < j ) } = {}
AA:
i in dom f
by FINSEQ_3:25, A1, A3, A4;
then mid (
f,
i,
j) =
<*(f . i)*>
by A4, JORDAN4:15
.=
<*(f /. i)*>
by AA, PARTFUN1:def 6
;
hence
L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }
by A5, SPPOL_2:12, ZFMISC_1:2;
verum end; suppose A7:
i < j
;
L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }
{ (LSeg ((mid (f,i,j)),m)) where m is Nat : ( 1 <= m & m + 1 <= len (mid (f,i,j)) ) } = { (LSeg (f,l)) where l is Nat : ( i <= l & l < j ) }
proof
hereby TARSKI:def 3,
XBOOLE_0:def 10 { (LSeg (f,l)) where l is Nat : ( i <= l & l < j ) } c= { (LSeg ((mid (f,i,j)),m)) where m is Nat : ( 1 <= m & m + 1 <= len (mid (f,i,j)) ) }
let x be
object ;
( x in { (LSeg ((mid (f,i,j)),m)) where m is Nat : ( 1 <= m & m + 1 <= len (mid (f,i,j)) ) } implies x in { (LSeg (f,l)) where l is Nat : ( i <= l & l < j ) } )assume
x in { (LSeg ((mid (f,i,j)),m)) where m is Nat : ( 1 <= m & m + 1 <= len (mid (f,i,j)) ) }
;
x in { (LSeg (f,l)) where l is Nat : ( i <= l & l < j ) } then consider m being
Nat such that A8:
x = LSeg (
(mid (f,i,j)),
m)
and A9:
0 + 1
<= m
and A10:
m + 1
<= len (mid (f,i,j))
;
i < m + i
by A9, XREAL_1:29;
then A11:
i <= (m + i) -' 1
by NAT_D:49;
len (mid (f,i,j)) = (j -' i) + 1
by A1, A3, A7, JORDAN4:8;
then A12:
m < (j -' i) + 1
by A10, NAT_1:13;
then
m <= j -' i
by NAT_1:13;
then
m <= j - i
by A7, XREAL_1:233;
then
(
m + i >= m &
m + i <= j )
by NAT_1:11, XREAL_1:19;
then
((m + i) -' 1) + 1
<= j
by A9, XREAL_1:235, XXREAL_0:2;
then A13:
(m + i) -' 1
< j
by NAT_1:13;
x = LSeg (
f,
((m + i) -' 1))
by A1, A3, A7, A8, A9, A12, JORDAN4:19;
hence
x in { (LSeg (f,l)) where l is Nat : ( i <= l & l < j ) }
by A13, A11;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in { (LSeg (f,l)) where l is Nat : ( i <= l & l < j ) } or x in { (LSeg ((mid (f,i,j)),m)) where m is Nat : ( 1 <= m & m + 1 <= len (mid (f,i,j)) ) } )
assume
x in { (LSeg (f,l)) where l is Nat : ( i <= l & l < j ) }
;
x in { (LSeg ((mid (f,i,j)),m)) where m is Nat : ( 1 <= m & m + 1 <= len (mid (f,i,j)) ) }
then consider l being
Nat such that A14:
x = LSeg (
f,
l)
and A15:
i <= l
and A16:
l < j
;
set m =
(l -' i) + 1;
A17:
l - i < j - i
by A16, XREAL_1:9;
(
l -' i = l - i &
j -' i = j - i )
by A15, A16, XREAL_1:233, XXREAL_0:2;
then A18:
(l -' i) + 1
< (j -' i) + 1
by A17, XREAL_1:6;
len (mid (f,i,j)) = (j -' i) + 1
by A1, A3, A7, JORDAN4:8;
then A19:
((l -' i) + 1) + 1
<= len (mid (f,i,j))
by A18, NAT_1:13;
A20:
1
<= (l -' i) + 1
by NAT_1:11;
(((l -' i) + 1) + i) -' 1 =
(((l -' i) + i) + 1) -' 1
.=
(l + 1) -' 1
by A15, XREAL_1:235
.=
l
by NAT_D:34
;
then
x = LSeg (
(mid (f,i,j)),
((l -' i) + 1))
by A1, A3, A7, A14, A20, A18, JORDAN4:19;
hence
x in { (LSeg ((mid (f,i,j)),m)) where m is Nat : ( 1 <= m & m + 1 <= len (mid (f,i,j)) ) }
by A20, A19;
verum
end; hence
L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }
;
verum end;