let A, B be non empty closed_interval Subset of REAL; :: thesis: for r being Real
for rho, rho1 being Function of A,REAL st B c= A & rho = r (#) rho1 holds
vol (B,rho) = r * (vol (B,rho1))
let r be Real; :: thesis: for rho, rho1 being Function of A,REAL st B c= A & rho = r (#) rho1 holds
vol (B,rho) = r * (vol (B,rho1))
let rho, rho1 be Function of A,REAL; :: thesis: ( B c= A & rho = r (#) rho1 implies vol (B,rho) = r * (vol (B,rho1)) )
assume AS: ( B c= A & rho = r (#) rho1 ) ; :: thesis: vol (B,rho) = r * (vol (B,rho1))
A2: dom (r (#) rho1) = A by FUNCT_2:def 1;
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) 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 C9: lower_bound B in B by A3, RCOMP_1:2;
thus vol (B,rho) = ((r (#) rho1) . (upper_bound B)) - ((r (#) rho1) . (lower_bound B)) by AS, Defvol
.= (r * (rho1 . (upper_bound B))) - ((r (#) rho1) . (lower_bound B)) by A2, AS, A8, VALUED_1:def 5
.= (r * (rho1 . (upper_bound B))) - (r * (rho1 . (lower_bound B))) by A2, AS, C9, VALUED_1:def 5
.= r * ((rho1 . (upper_bound B)) - (rho1 . (lower_bound B)))
.= r * (vol (B,rho1)) by Defvol ; :: thesis: verum