theorem Th18: :: INTEGR23:16

for A being non empty closed_interval Subset of REAL
for T being Division of A
for rho being real-valued Function
for B being non empty closed_interval Subset of REAL
for S0 being non empty increasing FinSequence of REAL
for ST being FinSequence of REAL st B c= A & lower_bound B = lower_bound A & ex S being Division of B st
( S = S0 & len ST = len S & ( for j being Nat st j in dom S holds
ex p being FinSequence of REAL st
( ST . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S,j))),rho)).| ) ) ) ) holds
ex H being Division of B ex F being var_volume of rho,H st Sum ST = Sum F