let i, j be Element of NAT ; :: thesis: 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 Element of NAT : ( i <= k & k < j ) }
let f be FinSequence of (TOP-REAL 2); :: thesis: ( 1 <= i & i <= j & j <= len f implies L~ (mid f,i,j) = union { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) } )
assume that
A1:
1 <= i
and
A2:
i <= j
and
A3:
j <= len f
; :: thesis: L~ (mid f,i,j) = union { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) }
set A = { (LSeg (mid f,i,j),m) where m is Element of NAT : ( 1 <= m & m + 1 <= len (mid f,i,j) ) } ;
set B = { (LSeg f,l) where l is Element of NAT : ( i <= l & l < j ) } ;
per cases
( i = j or i < j )
by A2, XXREAL_0:1;
suppose A4:
i = j
;
:: thesis: L~ (mid f,i,j) = union { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) } then A5:
mid f,
i,
j = <*(f /. i)*>
by A1, A3, JORDAN4:27;
{ (LSeg f,l) where l is Element of NAT : ( i <= l & l < j ) } = {}
hence
L~ (mid f,i,j) = union { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) }
by A5, SPPOL_2:12, ZFMISC_1:2;
:: thesis: verum end; suppose A7:
i < j
;
:: thesis: L~ (mid f,i,j) = union { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) }
{ (LSeg (mid f,i,j),m) where m is Element of NAT : ( 1 <= m & m + 1 <= len (mid f,i,j) ) } = { (LSeg f,l) where l is Element of NAT : ( i <= l & l < j ) }
proof
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: { (LSeg f,l) where l is Element of NAT : ( i <= l & l < j ) } c= { (LSeg (mid f,i,j),m) where m is Element of NAT : ( 1 <= m & m + 1 <= len (mid f,i,j) ) }
let x be
set ;
:: thesis: ( x in { (LSeg (mid f,i,j),m) where m is Element of NAT : ( 1 <= m & m + 1 <= len (mid f,i,j) ) } implies x in { (LSeg f,l) where l is Element of NAT : ( i <= l & l < j ) } )assume
x in { (LSeg (mid f,i,j),m) where m is Element of NAT : ( 1 <= m & m + 1 <= len (mid f,i,j) ) }
;
:: thesis: x in { (LSeg f,l) where l is Element of NAT : ( i <= l & l < j ) } then consider m being
Element of
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)
;
A11:
m + i >= m
by NAT_1:11;
len (mid f,i,j) = (j -' i) + 1
by A1, A3, A7, JORDAN4:20;
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:235;
then
m + i <= j
by XREAL_1:21;
then
((m + i) -' 1) + 1
<= j
by A9, A11, XREAL_1:237, XXREAL_0:2;
then A13:
(m + i) -' 1
< j
by NAT_1:13;
i < m + i
by A9, XREAL_1:31;
then A14:
i <= (m + i) -' 1
by NAT_D:49;
x = LSeg f,
((m + i) -' 1)
by A1, A3, A7, A8, A9, A12, JORDAN4:31;
hence
x in { (LSeg f,l) where l is Element of NAT : ( i <= l & l < j ) }
by A13, A14;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { (LSeg f,l) where l is Element of NAT : ( i <= l & l < j ) } or x in { (LSeg (mid f,i,j),m) where m is Element of NAT : ( 1 <= m & m + 1 <= len (mid f,i,j) ) } )
assume
x in { (LSeg f,l) where l is Element of NAT : ( i <= l & l < j ) }
;
:: thesis: x in { (LSeg (mid f,i,j),m) where m is Element of NAT : ( 1 <= m & m + 1 <= len (mid f,i,j) ) }
then consider l being
Element of
NAT such that A15:
x = LSeg f,
l
and A16:
i <= l
and A17:
l < j
;
set m =
(l -' i) + 1;
A18:
1
<= (l -' i) + 1
by NAT_1:11;
A19:
len (mid f,i,j) = (j -' i) + 1
by A1, A3, A7, JORDAN4:20;
A20:
(
l -' i = l - i &
j -' i = j - i )
by A16, A17, XREAL_1:235, XXREAL_0:2;
l - i < j - i
by A17, XREAL_1:11;
then A21:
(l -' i) + 1
< (j -' i) + 1
by A20, XREAL_1:8;
then A22:
((l -' i) + 1) + 1
<= len (mid f,i,j)
by A19, NAT_1:13;
(((l -' i) + 1) + i) -' 1 =
(((l -' i) + i) + 1) -' 1
.=
(l + 1) -' 1
by A16, XREAL_1:237
.=
l
by NAT_D:34
;
then
x = LSeg (mid f,i,j),
((l -' i) + 1)
by A1, A3, A7, A15, A18, A21, JORDAN4:31;
hence
x in { (LSeg (mid f,i,j),m) where m is Element of NAT : ( 1 <= m & m + 1 <= len (mid f,i,j) ) }
by A18, A22;
:: thesis: verum
end; hence
L~ (mid f,i,j) = union { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) }
;
:: thesis: verum end;