let r be Real; :: thesis: for i being Nat

for A being non empty 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_below & r <= 0 holds

(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

let i be Nat; :: thesis: for A being non empty 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_below & r <= 0 holds

(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

let A be non empty 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_below & r <= 0 holds

(upper_volume ((r (#) f),D)) . i = r * ((lower_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_below & r <= 0 holds

(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

let D be Division of A; :: thesis: ( i in dom D & f | A is bounded_below & r <= 0 implies (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) )

assume that

A1: i in dom D and

A2: f | A is bounded_below and

A3: r <= 0 ; :: thesis: (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) by RELAT_1:61

.= A /\ (divset (D,i)) by FUNCT_2:def 1

.= divset (D,i) by A1, INTEGRA1:8, XBOOLE_1:28 ;

then A4: not rng (f | (divset (D,i))) is empty by RELAT_1:42;

rng f is bounded_below by A2, INTEGRA1:11;

then A5: rng (f | (divset (D,i))) is bounded_below by RELAT_1:70, XXREAL_2:44;

(upper_volume ((r (#) f),D)) . i = (upper_bound (rng ((r (#) f) | (divset (D,i))))) * (vol (divset (D,i))) by A1, INTEGRA1:def 6

.= (upper_bound (rng (r (#) (f | (divset (D,i)))))) * (vol (divset (D,i))) by RFUNCT_1:49

.= (upper_bound (r ** (rng (f | (divset (D,i)))))) * (vol (divset (D,i))) by Th18

.= (r * (lower_bound (rng (f | (divset (D,i)))))) * (vol (divset (D,i))) by A3, A4, A5, Th16

.= r * ((lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))))

.= r * ((lower_volume (f,D)) . i) by A1, INTEGRA1:def 7 ;

hence (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) ; :: thesis: verum

for A being non empty 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_below & r <= 0 holds

(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

let i be Nat; :: thesis: for A being non empty 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_below & r <= 0 holds

(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

let A be non empty 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_below & r <= 0 holds

(upper_volume ((r (#) f),D)) . i = r * ((lower_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_below & r <= 0 holds

(upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

let D be Division of A; :: thesis: ( i in dom D & f | A is bounded_below & r <= 0 implies (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) )

assume that

A1: i in dom D and

A2: f | A is bounded_below and

A3: r <= 0 ; :: thesis: (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)

dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) by RELAT_1:61

.= A /\ (divset (D,i)) by FUNCT_2:def 1

.= divset (D,i) by A1, INTEGRA1:8, XBOOLE_1:28 ;

then A4: not rng (f | (divset (D,i))) is empty by RELAT_1:42;

rng f is bounded_below by A2, INTEGRA1:11;

then A5: rng (f | (divset (D,i))) is bounded_below by RELAT_1:70, XXREAL_2:44;

(upper_volume ((r (#) f),D)) . i = (upper_bound (rng ((r (#) f) | (divset (D,i))))) * (vol (divset (D,i))) by A1, INTEGRA1:def 6

.= (upper_bound (rng (r (#) (f | (divset (D,i)))))) * (vol (divset (D,i))) by RFUNCT_1:49

.= (upper_bound (r ** (rng (f | (divset (D,i)))))) * (vol (divset (D,i))) by Th18

.= (r * (lower_bound (rng (f | (divset (D,i)))))) * (vol (divset (D,i))) by A3, A4, A5, Th16

.= r * ((lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))))

.= r * ((lower_volume (f,D)) . i) by A1, INTEGRA1:def 7 ;

hence (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) ; :: thesis: verum