let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A
for f being Function of A,REAL holds (PartSums (lower_volume (f,D))) . (len D) = lower_sum (f,D)
let D be Division of A; :: thesis: for f being Function of A,REAL holds (PartSums (lower_volume (f,D))) . (len D) = lower_sum (f,D)
let f be Function of A,REAL; :: thesis: (PartSums (lower_volume (f,D))) . (len D) = lower_sum (f,D)
len (lower_volume (f,D)) = len D by Def6;
then len D in Seg (len (lower_volume (f,D))) by FINSEQ_1:3;
then len D in dom (lower_volume (f,D)) by FINSEQ_1:def 3;
then A1: (PartSums (lower_volume (f,D))) . (len D) = Sum ((lower_volume (f,D)) | (len D)) by Def19;
dom (lower_volume (f,D)) = Seg (len (lower_volume (f,D))) by FINSEQ_1:def 3;
then dom (lower_volume (f,D)) = Seg (len D) by Def6;
then (lower_volume (f,D)) | (Seg (len D)) = lower_volume (f,D) ;
hence (PartSums (lower_volume (f,D))) . (len D) = lower_sum (f,D) by A1, FINSEQ_1:def 16; :: thesis: verum