let A be non empty closed_interval Subset of REAL; :: thesis: 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)) )
let rho be Function of A,REAL; :: thesis: 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)) )
let u, w be PartFunc of REAL,REAL; :: thesis: ( rho is bounded_variation & dom u = A & dom w = A & w = - u & u is_RiemannStieltjes_integrable_with rho implies ( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = - (integral (u,rho)) ) )
assume A1: ( rho is bounded_variation & dom u = A & dom w = A & w = - u & u is_RiemannStieltjes_integrable_with rho ) ; :: thesis: ( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = - (integral (u,rho)) )
then A2: w = (- jj) (#) u by VALUED_1:def 6;
hence w is_RiemannStieltjes_integrable_with rho by A1, Th4; :: thesis: integral (w,rho) = - (integral (u,rho))
integral (w,rho) = (- jj) * (integral (u,rho)) by A1, A2, Th4;
hence integral (w,rho) = - (integral (u,rho)) ; :: thesis: verum