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)) = (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1)))
let f be FinSequence of (TOP-REAL 2); ( 1 <= i & i < j & j <= len f implies L~ (mid (f,i,j)) = (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1))) )
assume that
A1:
1 <= i
and
A2:
i < j
and
A3:
j <= len f
; L~ (mid (f,i,j)) = (L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1)))
j -' 1 <= j
by NAT_D:35;
then A4:
j -' 1 <= len f
by A3, XXREAL_0:2;
set A = { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } ;
set B = { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } ;
A5:
i <= j -' 1
by A2, NAT_D:49;
A6:
{ (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } = { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))}
proof
thus
{ (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } c= { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))}
XBOOLE_0:def 10 { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} c= { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } proof
let e be
object ;
TARSKI:def 3 ( not e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } or e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} )
assume
e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }
;
e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))}
then consider k being
Nat such that A7:
e = LSeg (
f,
k)
and A8:
i <= k
and A9:
k < j
;
k <= j -' 1
by A9, NAT_D:49;
then
(
j -' 1
= k or
k < j -' 1 )
by XXREAL_0:1;
then
(
e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } or
e in {(LSeg (f,(j -' 1)))} )
by A7, A8, TARSKI:def 1;
hence
e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))}
by XBOOLE_0:def 3;
verum
end;
let e be
object ;
TARSKI:def 3 ( not e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))} or e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } )
A10:
j -' 1
<= j
by NAT_D:35;
assume A11:
e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } \/ {(LSeg (f,(j -' 1)))}
;
e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }
end;
thus L~ (mid (f,i,j)) =
union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }
by A1, A2, A3, SPRECT_2:14
.=
(union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } ) \/ (union {(LSeg (f,(j -' 1)))})
by A6, ZFMISC_1:78
.=
(union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } ) \/ (LSeg (f,(j -' 1)))
by ZFMISC_1:25
.=
(L~ (mid (f,i,(j -' 1)))) \/ (LSeg (f,(j -' 1)))
by A1, A5, A4, SPRECT_2:14
; verum