let I be non empty closed_interval Subset of REAL; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( (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; :: thesis: (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; :: thesis: verum