let i, j be Element of 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 Element of NAT : ( i <= k & k < j ) } ;
set B = { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j -' 1 ) } ;
A5: i <= j -' 1 by A2, NAT_D:49;
A6: { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) } = { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg f,(j -' 1))}

proof

thus { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) } c= { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg f,(j -' 1))} :: according to XBOOLE_0:def 10 :: thesis: { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg f,(j -' 1))} c= { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) }

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) } or e in { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg f,(j -' 1))} )
assume e in { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) } ; :: thesis: e in { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg f,(j -' 1))}
then consider k being Element of 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 Element of 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 Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg f,(j -' 1))} by XBOOLE_0:def 3; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg f,(j -' 1))} or e in { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) } )
A10: j -' 1 <= j by NAT_D:35;
assume A11: e in { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j -' 1 ) } \/ {(LSeg f,(j -' 1))} ; :: thesis: e in { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) }

per cases ( e in { (LSeg f,k) where k is Element of 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 Element of NAT : ( i <= k & k < j -' 1 ) } ; :: thesis: e in { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j ) }

then consider k being Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT : ( i <= k & k < j ) } by A1, A2, A3, SPRECT_2:18
.= (union { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j -' 1 ) } ) \/ (union {(LSeg f,(j -' 1))}) by A6, ZFMISC_1:96
.= (union { (LSeg f,k) where k is Element of NAT : ( i <= k & k < j -' 1 ) } ) \/ (LSeg f,(j -' 1)) by ZFMISC_1:31
.= (L~ (mid f,i,(j -' 1))) \/ (LSeg f,(j -' 1)) by A1, A5, A4, SPRECT_2:18 ; :: thesis: verum