let j be Element of NAT ; 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; for D1 being Division of A st j in dom D1 holds
vol (divset (D1,j)) <= delta D1
let D1 be Division of A; ( j in dom D1 implies vol (divset (D1,j)) <= delta D1 )
assume A1:
j in dom D1
; 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
; verum