let j be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL
for D1 being Division of A st j in dom D1 holds
vol (divset D1,j) <= delta D1
let A be closed-interval Subset of REAL ; :: thesis: for D1 being Division of A st j in dom D1 holds
vol (divset D1,j) <= delta D1
let D1 be Division of A; :: thesis: ( j in dom D1 implies vol (divset D1,j) <= delta D1 )
assume A1: j in dom D1 ; :: thesis: vol (divset D1,j) <= delta D1
then j in Seg (len D1) by FINSEQ_1:def 3;
then j in Seg (len (upper_volume (chi A,A),D1)) by INTEGRA1:def 7;
then j in dom (upper_volume (chi A,A),D1) by FINSEQ_1:def 3;
then (upper_volume (chi A,A),D1) . j in rng (upper_volume (chi A,A),D1) by FUNCT_1:def 5;
then (upper_volume (chi A,A),D1) . j <= max (rng (upper_volume (chi A,A),D1)) by XXREAL_2:def 8;
then vol (divset D1,j) <= max (rng (upper_volume (chi A,A),D1)) by A1, INTEGRA1:22;
hence vol (divset D1,j) <= delta D1 ; :: thesis: verum