let A be closed-interval Subset of REAL ; :: thesis: for D being Division of A holds Sum (upper_volume (chi A,A),D) = vol A
let D be Division of A; :: thesis: Sum (upper_volume (chi A,A),D) = vol A
lower_volume (chi A,A),D = upper_volume (chi A,A),D

proof

A1: len (lower_volume (chi A,A),D) = len D by Def8
.= len (upper_volume (chi A,A),D) by Def7 ;
for i being Nat st 1 <= i & i <= len (lower_volume (chi A,A),D) holds
(lower_volume (chi A,A),D) . i = (upper_volume (chi A,A),D) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (lower_volume (chi A,A),D) implies (lower_volume (chi A,A),D) . i = (upper_volume (chi A,A),D) . i )
assume ( 1 <= i & i <= len (lower_volume (chi A,A),D) ) ; :: thesis: (lower_volume (chi A,A),D) . i = (upper_volume (chi A,A),D) . i
then ( 1 <= i & i <= len D ) by Def8;
then A2: i in dom D by FINSEQ_3:27;
then (lower_volume (chi A,A),D) . i = vol (divset D,i) by Th21
.= (upper_volume (chi A,A),D) . i by A2, Th22 ;
hence (lower_volume (chi A,A),D) . i = (upper_volume (chi A,A),D) . i ; :: thesis: verum

end;

hence lower_volume (chi A,A),D = upper_volume (chi A,A),D by A1, FINSEQ_1:18; :: thesis: verum

end;

hence Sum (upper_volume (chi A,A),D) = vol A by Th25; :: thesis: verum