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 (upper_volume (f,D))) . (len D) = upper_sum (f,D)
let D be Division of A; :: thesis: for f being Function of A,REAL holds (PartSums (upper_volume (f,D))) . (len D) = upper_sum (f,D)
let f be Function of A,REAL; :: thesis: (PartSums (upper_volume (f,D))) . (len D) = upper_sum (f,D)
len (upper_volume (f,D)) = len D by Def5;
then len D in Seg (len (upper_volume (f,D))) by FINSEQ_1:3;
then len D in dom (upper_volume (f,D)) by FINSEQ_1:def 3;
then A1: (PartSums (upper_volume (f,D))) . (len D) = Sum ((upper_volume (f,D)) | (len D)) by Def19;
dom (upper_volume (f,D)) = Seg (len (upper_volume (f,D))) by FINSEQ_1:def 3;
then dom (upper_volume (f,D)) = Seg (len D) by Def5;
then (upper_volume (f,D)) | (Seg (len D)) = upper_volume (f,D) ;
hence (PartSums (upper_volume (f,D))) . (len D) = upper_sum (f,D) by A1, FINSEQ_1:def 16; :: thesis: verum