let A be non empty closed_interval Subset of REAL; :: thesis: for rho being Function of A,REAL
for u, v, w being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & dom v = A & dom w = A & w = u - v & u is_RiemannStieltjes_integrable_with rho & v is_RiemannStieltjes_integrable_with rho holds
( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = (integral (u,rho)) - (integral (v,rho)) )
let rho be Function of A,REAL; :: thesis: for u, v, w being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & dom v = A & dom w = A & w = u - v & u is_RiemannStieltjes_integrable_with rho & v is_RiemannStieltjes_integrable_with rho holds
( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = (integral (u,rho)) - (integral (v,rho)) )
let u, v, w be PartFunc of REAL,REAL; :: thesis: ( rho is bounded_variation & dom u = A & dom v = A & dom w = A & w = u - v & u is_RiemannStieltjes_integrable_with rho & v is_RiemannStieltjes_integrable_with rho implies ( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = (integral (u,rho)) - (integral (v,rho)) ) )
assume A1: ( rho is bounded_variation & dom u = A & dom v = A & dom w = A & w = u - v & u is_RiemannStieltjes_integrable_with rho & v is_RiemannStieltjes_integrable_with rho ) ; :: thesis: ( w is_RiemannStieltjes_integrable_with rho & integral (w,rho) = (integral (u,rho)) - (integral (v,rho)) )
then A2: w = u + (- v) by VALUED_1:def 9;
A3: dom (- v) = A by A1, VALUED_1:8;
reconsider gg = - v as PartFunc of REAL,REAL ;
A5: gg is_RiemannStieltjes_integrable_with rho by A1, Th5, A3;
hence w is_RiemannStieltjes_integrable_with rho by A1, A2, Th6, A3; :: thesis: integral (w,rho) = (integral (u,rho)) - (integral (v,rho))
integral (w,rho) = (integral (u,rho)) + (integral (gg,rho)) by A1, A2, A5, Th6, A3;
then integral (w,rho) = (integral (u,rho)) + (- (integral (v,rho))) by A1, Th5, A3;
hence integral (w,rho) = (integral (u,rho)) - (integral (v,rho)) ; :: thesis: verum