let i be Element of NAT ; :: thesis: for A being 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 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 Def8;
divset D,i c= A by A2, Th10;
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) by XBOOLE_0:def 7;
then A4: rng ((chi A,A) | (divset D,i)) = {1} by Th20;
A5: rng (chi A,A) = {1} by Th19;
then lower_bound (rng (chi A,A)) = 1 by SEQ_4:22;
hence vol (divset D,i) = (lower_volume (chi A,A),D) . i by A3, A5, A4; :: thesis: verum