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))}

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

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

A12:
1 <= i + 1
by NAT_1:11;
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 ) }

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 ) }

end;proof

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 ) } )
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;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

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;

end;

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;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

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