theorem Th21:
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 )