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))
A1: ( dom rho1 = A & dom rho2 = A ) by FUNCT_2:def 1;
A2: dom (rho1 + rho2) = (dom rho1) /\ (dom rho2) by VALUED_1:def 1
.= A by A1 ;
set x1 = upper_bound B;
set x2 = lower_bound B;
A3: B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:4;
A5: (upper_bound B) - (lower_bound B) >= 0 by XREAL_1:48, SEQ_4:11;
|.((lower_bound B) - (upper_bound B)).| = (upper_bound B) - (lower_bound B)

proof

per cases ( (lower_bound B) - (upper_bound B) < 0 or (lower_bound B) - (upper_bound B) = 0 ) by SEQ_4:11, XREAL_1:47;

suppose (lower_bound B) - (upper_bound B) < 0 ; :: thesis: |.((lower_bound B) - (upper_bound B)).| = (upper_bound B) - (lower_bound B)

hence |.((lower_bound B) - (upper_bound B)).| = - ((lower_bound B) - (upper_bound B)) by ABSVALUE:def 1
.= (upper_bound B) - (lower_bound B) ;
:: thesis: verum

end;

suppose (lower_bound B) - (upper_bound B) = 0 ; :: thesis: |.((lower_bound B) - (upper_bound B)).| = (upper_bound B) - (lower_bound B)

hence |.((lower_bound B) - (upper_bound B)).| = (upper_bound B) - (lower_bound B) by COMPLEX1:44; :: thesis: verum

end;

end;

end;

then |.(((upper_bound B) + (lower_bound B)) - (2 * (upper_bound B))).| = (upper_bound B) - (lower_bound B) ;
then A8: upper_bound B in B by A3, RCOMP_1:2;
|.(((upper_bound B) + (lower_bound B)) - (2 * (lower_bound B))).| = (upper_bound B) - (lower_bound B) by A5, ABSVALUE:def 1;
then B9: lower_bound B in B by A3, RCOMP_1:2;
thus vol (B,rho) = ((rho1 + rho2) . (upper_bound B)) - ((rho1 + rho2) . (lower_bound B)) by AS, Defvol
.= ((rho1 . (upper_bound B)) + (rho2 . (upper_bound B))) - ((rho1 + rho2) . (lower_bound B)) by A2, AS, A8, VALUED_1:def 1
.= ((rho1 . (upper_bound B)) + (rho2 . (upper_bound B))) - ((rho1 . (lower_bound B)) + (rho2 . (lower_bound B))) by B9, A2, AS, VALUED_1:def 1
.= ((rho1 . (upper_bound B)) - (rho1 . (lower_bound B))) + ((rho2 . (upper_bound B)) - (rho2 . (lower_bound B)))
.= (vol (B,rho1)) + ((rho2 . (upper_bound B)) - (rho2 . (lower_bound B))) by Defvol
.= (vol (B,rho1)) + (vol (B,rho2)) by Defvol ; :: thesis: verum