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 holds
( Sum (lower_volume (f,(division_of TD))) <= Sum (tagged_volume (f,TD)) & Sum (tagged_volume (f,TD)) <= Sum (upper_volume (f,(division_of TD))) )
let TD be tagged_division of I; :: thesis: for f being bounded integrable Function of I,REAL holds
( Sum (lower_volume (f,(division_of TD))) <= Sum (tagged_volume (f,TD)) & Sum (tagged_volume (f,TD)) <= Sum (upper_volume (f,(division_of TD))) )
let f be bounded integrable Function of I,REAL; :: thesis: ( Sum (lower_volume (f,(division_of TD))) <= Sum (tagged_volume (f,TD)) & Sum (tagged_volume (f,TD)) <= Sum (upper_volume (f,(division_of TD))) )
A1: len (tagged_volume (f,TD)) = len TD by Def4
.= len (lower_volume (f,(division_of TD))) by INTEGRA1:def 7 ;
dom TD = Seg (len (division_of TD)) by FINSEQ_1:def 3
.= Seg (len (lower_volume (f,(division_of TD)))) by INTEGRA1:def 7
.= dom (lower_volume (f,(division_of TD))) by FINSEQ_1:def 3 ;
then for i being Element of NAT st i in dom (lower_volume (f,(division_of TD))) holds
(lower_volume (f,(division_of TD))) . i <= (tagged_volume (f,TD)) . i by Th39;
hence Sum (lower_volume (f,(division_of TD))) <= Sum (tagged_volume (f,TD)) by INTEGRA5:3, A1; :: thesis: Sum (tagged_volume (f,TD)) <= Sum (upper_volume (f,(division_of TD)))
B1: len (tagged_volume (f,TD)) = len TD by Def4
.= len (upper_volume (f,(division_of TD))) by INTEGRA1:def 6 ;
dom TD = Seg (len TD) by FINSEQ_1:def 3
.= Seg (len (tagged_volume (f,TD))) by Def4
.= dom (tagged_volume (f,TD)) by FINSEQ_1:def 3 ;
then for i being Element of NAT st i in dom (tagged_volume (f,TD)) holds
(tagged_volume (f,TD)) . i <= (upper_volume (f,(division_of TD))) . i by Th39;
hence Sum (tagged_volume (f,TD)) <= Sum (upper_volume (f,(division_of TD))) by INTEGRA5:3, B1; :: thesis: verum