let A be 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 Def8;
then len D in Seg (len (lower_volume f,D)) by FINSEQ_1:5;
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 Def22;
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 Def8;
then (lower_volume f,D) | (Seg (len D)) = lower_volume f,D by RELAT_1:97;
hence (PartSums (lower_volume f,D)) . (len D) = lower_sum f,D by A1, FINSEQ_1:def 15; :: thesis: verum