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;

then vol (divset (D1,j)) <= max (rng (upper_volume ((chi (A,A)),D1))) by A1, INTEGRA1:20;

hence vol (divset (D1,j)) <= delta D1 ; :: thesis: verum

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;

then vol (divset (D1,j)) <= max (rng (upper_volume ((chi (A,A)),D1))) by A1, INTEGRA1:20;

hence vol (divset (D1,j)) <= delta D1 ; :: thesis: verum