let r be Real; :: thesis: for i being Element of NAT
for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds
(lower_volume (r (#) f),D) . i = r * ((upper_volume f,D) . i)
let i be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds
(lower_volume (r (#) f),D) . i = r * ((upper_volume f,D) . i)
let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds
(lower_volume (r (#) f),D) . i = r * ((upper_volume f,D) . i)
let f be Function of A,REAL ; :: thesis: for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds
(lower_volume (r (#) f),D) . i = r * ((upper_volume f,D) . i)
let D be Division of A; :: thesis: ( i in dom D & f | A is bounded_above & r <= 0 implies (lower_volume (r (#) f),D) . i = r * ((upper_volume f,D) . i) )
assume that
A1: i in dom D and
A2: f | A is bounded_above and
A3: r <= 0 ; :: thesis: (lower_volume (r (#) f),D) . i = r * ((upper_volume f,D) . i)
dom (f | (divset D,i)) = (dom f) /\ (divset D,i) by RELAT_1:90
.= A /\ (divset D,i) by FUNCT_2:def 1
.= divset D,i by A1, INTEGRA1:10, XBOOLE_1:28 ;
then A5: not rng (f | (divset D,i)) is empty by RELAT_1:65;
X: rng (f | (divset D,i)) c= rng f by RELAT_1:99;
rng f is bounded_above by A2, INTEGRA1:15;
then A6: rng (f | (divset D,i)) is bounded_above by X, XXREAL_2:43;
(lower_volume (r (#) f),D) . i = (lower_bound (rng ((r (#) f) | (divset D,i)))) * (vol (divset D,i)) by A1, INTEGRA1:def 8
.= (lower_bound (rng (r (#) (f | (divset D,i))))) * (vol (divset D,i)) by RFUNCT_1:65
.= (lower_bound (r ** (rng (f | (divset D,i))))) * (vol (divset D,i)) by Th18
.= (r * (upper_bound (rng (f | (divset D,i))))) * (vol (divset D,i)) by A3, A5, A6, Th14
.= r * ((upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)))
.= r * ((upper_volume f,D) . i) by A1, INTEGRA1:def 7 ;
hence (lower_volume (r (#) f),D) . i = r * ((upper_volume f,D) . i) ; :: thesis: verum