theorem Th17: :: INTEGR20:17

for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for h being Function of A, the carrier of X
for T0, T, T1 being DivSequence of A
for S0 being middle_volume_Sequence of h,T0
for S being middle_volume_Sequence of h,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 h,T1 st
for i being Nat holds
( S1 . (2 * i) = S0 . i & S1 . ((2 * i) + 1) = S . i )