let A be non empty closed_interval Subset of REAL; for D being Division of A holds Sum (upper_volume ((chi (A,A)),D)) = vol A
let D be Division of A; 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;
( 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))
;
(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
;
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; verum