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)) = union { (LSeg (f,k)) where k is 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 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 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 ; :: thesis: 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 ) } = {}

proof

assume { (LSeg (f,l)) where l is Nat : ( i <= l & l < j ) } <> {} ; :: thesis: contradiction
then consider z being object such that
A6: z in { (LSeg (f,l)) where l is Nat : ( i <= l & l < j ) } by XBOOLE_0:def 1;
ex l being Nat st
( z = LSeg (f,l) & i <= l & l < j ) by A6;
hence contradiction by A4; :: thesis: verum

end;

AA: i in dom f by FINSEQ_3:25, A1, A3, A4;
then mid (f,i,j) = <*(f . i)*> by A4, FINSEQ_6:193
.= <*(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; :: thesis: verum

end;

suppose A7: i < j ; :: thesis: 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 :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (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 ; :: thesis: ( 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)) ) } ; :: thesis: 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, FINSEQ_6:186;
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; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ) } ; :: thesis: 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, FINSEQ_6:186;
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; :: thesis: verum

end;

hence L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } ; :: thesis: verum

end;

end;