let i be Element of NAT ; for A being non empty closed_interval Subset of REAL
for D being Division of A st i in dom D holds
vol (divset (D,i)) = (lower_volume ((chi (A,A)),D)) . i
let A be non empty closed_interval Subset of REAL; for D being Division of A st i in dom D holds
vol (divset (D,i)) = (lower_volume ((chi (A,A)),D)) . i
let D be Division of A; ( i in dom D implies vol (divset (D,i)) = (lower_volume ((chi (A,A)),D)) . i )
A1:
dom (chi (A,A)) = A
by FUNCT_3:def 3;
assume A2:
i in dom D
; vol (divset (D,i)) = (lower_volume ((chi (A,A)),D)) . i
then A3:
(lower_volume ((chi (A,A)),D)) . i = (lower_bound (rng ((chi (A,A)) | (divset (D,i))))) * (vol (divset (D,i)))
by Def6;
divset (D,i) c= A
by A2, Th6;
then
divset (D,i) c= (divset (D,i)) /\ (dom (chi (A,A)))
by A1, XBOOLE_1:19;
then
(divset (D,i)) /\ (dom (chi (A,A))) <> {}
;
then
divset (D,i) meets dom (chi (A,A))
;
then A4:
rng ((chi (A,A)) | (divset (D,i))) = {1}
by Th16;
A5:
rng (chi (A,A)) = {1}
by Th15;
then
lower_bound (rng (chi (A,A))) = 1
by SEQ_4:9;
hence
vol (divset (D,i)) = (lower_volume ((chi (A,A)),D)) . i
by A3, A5, A4; verum