let A be non empty 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, Def6;
then A4: i in dom D by A2, FINSEQ_3:25;
then (lower_volume ((chi (A,A)),D)) . i = vol (divset (D,i)) by Th17
.= (upper_volume ((chi (A,A)),D)) . i by A4, Th18 ;
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 Def6
.= len (upper_volume ((chi (A,A)),D)) by Def5 ;
then lower_volume ((chi (A,A)),D) = upper_volume ((chi (A,A)),D) by A1, FINSEQ_1:14;
hence Sum (upper_volume ((chi (A,A)),D)) = vol A by Th21; :: thesis: verum