let A, B be non empty closed_interval Subset of REAL; :: thesis: for rho, rho1, rho2 being Function of A,REAL st B c= A & rho = rho1 - rho2 holds
vol (B,rho) = (vol (B,rho1)) - (vol (B,rho2))
let rho, rho1, rho2 be Function of A,REAL; :: thesis: ( B c= A & rho = rho1 - rho2 implies vol (B,rho) = (vol (B,rho1)) - (vol (B,rho2)) )
assume AS: ( B c= A & rho = rho1 - rho2 ) ; :: thesis: vol (B,rho) = (vol (B,rho1)) - (vol (B,rho2))
then A1: rho = rho1 + (- rho2) by VALUED_1:def 9;
set x1 = upper_bound B;
set x2 = lower_bound B;
thus vol (B,rho) = (vol (B,rho1)) + (vol (B,(- rho2))) by AS, A1, Lm6A
.= (vol (B,rho1)) + (((- rho2) . (upper_bound B)) - ((- rho2) . (lower_bound B))) by Defvol
.= (vol (B,rho1)) + ((- (rho2 . (upper_bound B))) - ((- rho2) . (lower_bound B))) by VALUED_1:8
.= (vol (B,rho1)) + ((- (rho2 . (upper_bound B))) - (- (rho2 . (lower_bound B)))) by VALUED_1:8
.= (vol (B,rho1)) - ((rho2 . (upper_bound B)) - (rho2 . (lower_bound B)))
.= (vol (B,rho1)) - (vol (B,rho2)) by Defvol ; :: thesis: verum