theorem Th5: :: INTEGR22:8

for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u, w being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & dom w = A & w = - u & u is_RiemannStieltjes_integrable_with rho holds
( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = - (integral (u,rho)) )