let i be Element of NAT ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum