let i, j be Nat; :: thesis: ( 1 <= i & i < j implies for f being FinSequence of (TOP-REAL 2) st j <= len f holds
L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j))) )
assume that
A1: 1 <= i and
A2: i < j ; :: thesis: for f being FinSequence of (TOP-REAL 2) st j <= len f holds
L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j)))
let f be FinSequence of (TOP-REAL 2); :: thesis: ( j <= len f implies L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j))) )
assume A3: j <= len f ; :: thesis: L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j)))
set A = { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } ;
set B = { (LSeg (f,k)) where k is Nat : ( i + 1 <= k & k < j ) } ;
A4: { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } = { (LSeg (f,k)) where k is Nat : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))}

proof

thus { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } c= { (LSeg (f,k)) where k is Nat : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} :: according to XBOOLE_0:def 10 :: thesis: { (LSeg (f,k)) where k is Nat : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} 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 + 1 <= k & k < j ) } \/ {(LSeg (f,i))} )
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 + 1 <= k & k < j ) } \/ {(LSeg (f,i))}
then consider k being Nat such that
A5: e = LSeg (f,k) and
A6: i <= k and
A7: k < j ;
( i = k or i < k ) by A6, XXREAL_0:1;
then ( i = k or i + 1 <= k ) by NAT_1:13;
then ( e in { (LSeg (f,k)) where k is Nat : ( i + 1 <= k & k < j ) } or e in {(LSeg (f,i))} ) by A5, A7, TARSKI:def 1;
hence e in { (LSeg (f,k)) where k is Nat : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} 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 + 1 <= k & k < j ) } \/ {(LSeg (f,i))} or e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } )
assume A8: e in { (LSeg (f,k)) where k is Nat : ( i + 1 <= k & k < j ) } \/ {(LSeg (f,i))} ; :: 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 + 1 <= k & k < j ) } or e in {(LSeg (f,i))} ) by A8, XBOOLE_0:def 3;

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

then consider k being Nat such that
A9: e = LSeg (f,k) and
A10: i + 1 <= k and
A11: k < j ;
i < k by A10, NAT_1:13;
hence e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } by A9, A11; :: thesis: verum

end;

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

then e = LSeg (f,i) by TARSKI:def 1;
hence e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } by A2; :: thesis: verum

end;

end;

end;

A12: 1 <= i + 1 by NAT_1:11;
A13: i + 1 <= j by A2, NAT_1:13;
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 + 1 <= k & k < j ) } ) \/ (union {(LSeg (f,i))}) by A4, ZFMISC_1:78
.= (union { (LSeg (f,k)) where k is Nat : ( i + 1 <= k & k < j ) } ) \/ (LSeg (f,i)) by ZFMISC_1:25
.= (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j))) by A3, A12, A13, SPRECT_2:14 ; :: thesis: verum