let i, j be Nat; :: thesis: ( 1 <= i & i < j implies for f being FinSequence of () 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 () st j <= len f holds
L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j)))

let f be FinSequence of (); :: 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 ;
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 ;
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 ;
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 ;
hence e in { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } by ; :: 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 ;
thus L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) } by
.= (union { (LSeg (f,k)) where k is Nat : ( i + 1 <= k & k < j ) } ) \/ (union {(LSeg (f,i))}) by
.= (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 ; :: thesis: verum