let j be Element of NAT ; :: thesis: for A being non empty 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 non empty 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 6;
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 3;
then (upper_volume ((chi (A,A)),D1)) . j <= max (rng (upper_volume ((chi (A,A)),D1))) by XXREAL_2:def 8;
hence vol (divset (D1,j)) <= delta D1 by A1, INTEGRA1:20; :: thesis: verum