let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A, REAL
for S being non empty Division of A
for D being Element of S
for i being Element of NAT st f | A is bounded_above & i in dom D holds
(upper_bound (rng f)) * (vol (divset D,i)) >= (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i))
let f be Function of A, REAL ; :: thesis: for S being non empty Division of A
for D being Element of S
for i being Element of NAT st f | A is bounded_above & i in dom D holds
(upper_bound (rng f)) * (vol (divset D,i)) >= (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i))
let S be non empty Division of A; :: thesis: for D being Element of S
for i being Element of NAT st f | A is bounded_above & i in dom D holds
(upper_bound (rng f)) * (vol (divset D,i)) >= (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i))
let D be Element of S; :: thesis: for i being Element of NAT st f | A is bounded_above & i in dom D holds
(upper_bound (rng f)) * (vol (divset D,i)) >= (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i))
let i be Element of NAT ; :: thesis: ( f | A is bounded_above & i in dom D implies (upper_bound (rng f)) * (vol (divset D,i)) >= (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) )
assume A1: f | A is bounded_above ; :: thesis: ( not i in dom D or (upper_bound (rng f)) * (vol (divset D,i)) >= (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) )
assume A2: i in dom D ; :: thesis: (upper_bound (rng f)) * (vol (divset D,i)) >= (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i))
A3: rng (f | (divset D,i)) c= rng f by RELAT_1:99;
A4: rng (f | (divset D,i)) is non empty Subset of REAL

proof

A5: dom f = A by FUNCT_2:def 1;
dom (f | (divset D,i)) = divset D,i by A5, Th10, A2, RELAT_1:91;
hence rng (f | (divset D,i)) is non empty Subset of REAL by RELAT_1:65; :: thesis: verum

end;

A6: rng f is bounded_above by A1, Th15;
0 <= vol (divset D,i) by SEQ_4:24, XREAL_1:50;
hence (upper_bound (rng f)) * (vol (divset D,i)) >= (upper_bound (rng (f | (divset D,i)))) * (vol (divset D,i)) by A3, A4, A6, SEQ_4:65, XREAL_1:66; :: thesis: verum