for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u being PartFunc of REAL,REAL
for T0, T, T1 being DivSequence of A
for S0 being middle_volume_Sequence of rho,u,T0
for S being middle_volume_Sequence of rho,u,T st ( for i being Nat holds
( T1 . (2 * i) = T0 . i & T1 . ((2 * i) + 1) = T . i ) ) holds
ex S1 being middle_volume_Sequence of rho,u,T1 st
for i being Nat holds
( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )