let I be non empty closed_interval Subset of REAL; for TD being tagged_division of I
for f being bounded integrable Function of I,REAL
for i being Nat st i in dom TD holds
( (lower_volume (f,(division_of TD))) . i <= (tagged_volume (f,TD)) . i & (tagged_volume (f,TD)) . i <= (upper_volume (f,(division_of TD))) . i )
let TD be tagged_division of I; for f being bounded integrable Function of I,REAL
for i being Nat st i in dom TD holds
( (lower_volume (f,(division_of TD))) . i <= (tagged_volume (f,TD)) . i & (tagged_volume (f,TD)) . i <= (upper_volume (f,(division_of TD))) . i )
let f be bounded integrable Function of I,REAL; for i being Nat st i in dom TD holds
( (lower_volume (f,(division_of TD))) . i <= (tagged_volume (f,TD)) . i & (tagged_volume (f,TD)) . i <= (upper_volume (f,(division_of TD))) . i )
let i be Nat; ( i in dom TD implies ( (lower_volume (f,(division_of TD))) . i <= (tagged_volume (f,TD)) . i & (tagged_volume (f,TD)) . i <= (upper_volume (f,(division_of TD))) . i ) )
assume A1:
i in dom TD
; ( (lower_volume (f,(division_of TD))) . i <= (tagged_volume (f,TD)) . i & (tagged_volume (f,TD)) . i <= (upper_volume (f,(division_of TD))) . i )
set a = (lower_volume (f,(division_of TD))) . i;
set b = (tagged_volume (f,TD)) . i;
set c = (upper_volume (f,(division_of TD))) . i;
reconsider D = division_of TD as Division of I ;
set x = (tagged_of TD) . i;
consider D9 being Division of I, T9 being Element of set_of_tagged_Division D9 such that
A2:
( tagged_of TD = T9 & TD = [D9,T9] )
by Def2;
A3:
( D = D9 & (tagged_of TD) . i = T9 . i )
by A2, Th20;
consider s being non empty non-decreasing FinSequence of REAL such that
A4:
( T9 = s & dom s = dom D9 & ( for i being Nat st i in dom s holds
s . i in divset (D9,i) ) )
by COUSIN:def 2;
divset (D,i) c= I
by A1, INTEGRA1:8;
then
(tagged_of TD) . i in I
by A1, A3, A4;
then A5:
(tagged_of TD) . i in dom f
by FUNCT_2:def 1;
then reconsider y = f . ((tagged_of TD) . i) as Element of REAL by PARTFUN1:4;
f /. ((tagged_of TD) . i) in rng (f | (divset (D,i)))
by A1, A3, A4, A5, PARTFUN2:18;
then W1:
f . ((tagged_of TD) . i) in rng (f | (divset (D,i)))
by A5, PARTFUN1:def 6;
rng f is bounded_below
by INTEGRA1:11;
then
rng (f | (divset (D,i))) is bounded_below
by RELAT_1:70, XXREAL_2:44;
then W3:
lower_bound (rng (f | (divset (D,i)))) <= f . ((tagged_of TD) . i)
by SEQ_4:def 2, W1;
0 <= vol (divset (D,i))
by INTEGRA1:9;
then
(lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) <= (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))
by XREAL_1:64, W3;
then
(lower_volume (f,D)) . i <= (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i)))
by A1, INTEGRA1:def 7;
hence
(lower_volume (f,(division_of TD))) . i <= (tagged_volume (f,TD)) . i
by A1, Def4; (tagged_volume (f,TD)) . i <= (upper_volume (f,(division_of TD))) . i
f /. ((tagged_of TD) . i) in rng (f | (divset (D,i)))
by A1, A3, A4, A5, PARTFUN2:18;
then T2:
f . ((tagged_of TD) . i) in rng (f | (divset (D,i)))
by A5, PARTFUN1:def 6;
rng f is bounded_above
by INTEGRA1:13;
then
rng (f | (divset (D,i))) is bounded_above
by RELAT_1:70, XXREAL_2:43;
then W1:
f . ((tagged_of TD) . i) <= upper_bound (rng (f | (divset (D,i))))
by SEQ_4:def 1, T2;
0 <= vol (divset (D,i))
by INTEGRA1:9;
then
(f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) <= (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i)))
by W1, XREAL_1:64;
then
(f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) <= (upper_volume (f,D)) . i
by A1, INTEGRA1:def 6;
hence
(tagged_volume (f,TD)) . i <= (upper_volume (f,(division_of TD))) . i
by A1, Def4; verum