let A be non empty closed_interval Subset of REAL; :: thesis: for rho, rho1 being Function of A,REAL
for u being PartFunc of REAL,REAL st rho is bounded_variation & rho1 is bounded_variation & dom u = A & rho = - rho1 & u is_RiemannStieltjes_integrable_with rho1 holds
( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = - (integral (u,rho1)) )
let rho, rho1 be Function of A,REAL; :: thesis: for u being PartFunc of REAL,REAL st rho is bounded_variation & rho1 is bounded_variation & dom u = A & rho = - rho1 & u is_RiemannStieltjes_integrable_with rho1 holds
( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = - (integral (u,rho1)) )
let u be PartFunc of REAL,REAL; :: thesis: ( rho is bounded_variation & rho1 is bounded_variation & dom u = A & rho = - rho1 & u is_RiemannStieltjes_integrable_with rho1 implies ( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = - (integral (u,rho1)) ) )
assume A1: ( rho is bounded_variation & rho1 is bounded_variation & dom u = A & rho = - rho1 & u is_RiemannStieltjes_integrable_with rho1 ) ; :: thesis: ( u is_RiemannStieltjes_integrable_with rho & integral (u,rho) = - (integral (u,rho1)) )
then A2: rho = (- jj) (#) rho1 by VALUED_1:def 6;
hence u is_RiemannStieltjes_integrable_with rho by A1, Th4A; :: thesis: integral (u,rho) = - (integral (u,rho1))
integral (u,rho) = (- jj) * (integral (u,rho1)) by A1, A2, Th4A;
hence integral (u,rho) = - (integral (u,rho1)) ; :: thesis: verum