let i, j be Nat; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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)))} :: according to XBOOLE_0:def 10 :: thesis: { (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 ; :: according to TARSKI:def 3 :: thesis: ( 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 ) } ; :: thesis: 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; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( 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)))} ; :: thesis: e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }

per cases ( e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } or e in {(LSeg (f,(j -' 1)))} ) by A11, XBOOLE_0:def 3;

suppose e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j -' 1 ) } ; :: thesis: e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }

then consider k being Nat such that
A12: e = LSeg (f,k) and
A13: i <= k and
A14: k < j -' 1 ;
k < j by A10, A14, XXREAL_0:2;
hence e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } by A12, A13; :: thesis: verum

end;

suppose A15: e in {(LSeg (f,(j -' 1)))} ; :: thesis: e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }

1 <= j -' 1 by A1, A5, XXREAL_0:2;
then A16: j -' 1 < j by NAT_D:51;
e = LSeg (f,(j -' 1)) by A15, TARSKI:def 1;
hence e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } by A5, A16; :: thesis: verum

end;

end;

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 ; :: thesis: verum