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
A1: 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 that
A2: 1 <= i and
A3: i <= len (lower_volume (chi A,A),D) ; :: thesis: (lower_volume (chi A,A),D) . i = (upper_volume (chi A,A),D) . i
i <= len D by A3, Def8;
then A4: i in dom D by A2, 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 A4, Th22 ;
hence (lower_volume (chi A,A),D) . i = (upper_volume (chi A,A),D) . i ; :: thesis: verum

end;

len (lower_volume (chi A,A),D) = len D by Def8
.= len (upper_volume (chi A,A),D) by Def7 ;
then lower_volume (chi A,A),D = upper_volume (chi A,A),D by A1, FINSEQ_1:18;
hence Sum (upper_volume (chi A,A),D) = vol A by Th25; :: thesis: verum