let I be non empty closed_interval Subset of REAL; :: thesis: for r being Real
for jauge being positive-yielding Function of I,REAL
for D being tagged_division of I st jauge = r (#) (chi (I,I)) & D is jauge -fine holds
delta (division_of D) <= r
let r be Real; :: thesis: for jauge being positive-yielding Function of I,REAL
for D being tagged_division of I st jauge = r (#) (chi (I,I)) & D is jauge -fine holds
delta (division_of D) <= r
let jauge be positive-yielding Function of I,REAL; :: thesis: for D being tagged_division of I st jauge = r (#) (chi (I,I)) & D is jauge -fine holds
delta (division_of D) <= r
let D be tagged_division of I; :: thesis: ( jauge = r (#) (chi (I,I)) & D is jauge -fine implies delta (division_of D) <= r )
assume that
A1: jauge = r (#) (chi (I,I)) and
A2: D is jauge -fine ; :: thesis: delta (division_of D) <= r

A3: now :: thesis: for i being Nat st i in dom (division_of D) holds
vol (divset ((division_of D),i)) <= r

let i be Nat; :: thesis: ( i in dom (division_of D) implies vol (divset ((division_of D),i)) <= r )
assume A4: i in dom (division_of D) ; :: thesis: vol (divset ((division_of D),i)) <= r
consider D9 being Division of I, T9 being Element of set_of_tagged_Division D9 such that
A5: ( D = [D9,T9] & ( for i being Nat st i in dom D9 holds
vol (divset (D9,i)) <= jauge . (T9 . i) ) ) by A2, COUSIN:def 4;
A6: ( T9 = tagged_of D & D9 = division_of D ) by A5, Th20;
then A7: vol (divset ((division_of D),i)) <= jauge . ((tagged_of D) . i) by A5, A4;
A8: dom (r (#) (chi (I,I))) = dom (chi (I,I)) by VALUED_1:def 5
.= I by FUNCT_3:def 3 ;
i in Seg (len (division_of D)) by A4, FINSEQ_1:def 3;
then i in Seg (len (tagged_of D)) by Th21;
then A9: i in dom T9 by A6, FINSEQ_1:def 3;
rng T9 c= I by Th22;
then A10: (tagged_of D) . i in I by A9, A6, FUNCT_1:3;

now :: thesis: for x being object st x in dom (r (#) (chi (I,I))) holds
jauge . x = r

let x be object ; :: thesis: ( x in dom (r (#) (chi (I,I))) implies jauge . x = r )
assume A11: x in dom (r (#) (chi (I,I))) ; :: thesis: jauge . x = r
then (r (#) (chi (I,I))) . x = r * ((chi (I,I)) . x) by VALUED_1:def 5
.= r * 1 by A11, FUNCT_3:def 3
.= r ;
hence jauge . x = r by A1; :: thesis: verum

end;

hence vol (divset ((division_of D),i)) <= r by A7, A8, A10; :: thesis: verum

end;

reconsider g = chi (I,I) as Function of I,REAL by Th11;
A12: for i being Nat st i in dom (division_of D) holds
(upper_volume (g,(division_of D))) . i <= r

proof

let i be Nat; :: thesis: ( i in dom (division_of D) implies (upper_volume (g,(division_of D))) . i <= r )
assume A13: i in dom (division_of D) ; :: thesis: (upper_volume (g,(division_of D))) . i <= r
then vol (divset ((division_of D),i)) <= r by A3;
hence (upper_volume (g,(division_of D))) . i <= r by A13, INTEGRA1:20; :: thesis: verum

end;

delta (division_of D) <= r

proof

assume r < delta (division_of D) ; :: thesis: contradiction
then A14: r < max (rng (upper_volume (g,(division_of D)))) by INTEGRA3:def 1;
sup (rng (upper_volume (g,(division_of D)))) in rng (upper_volume (g,(division_of D))) by XXREAL_2:def 6;
then consider x being object such that
A15: x in dom (upper_volume (g,(division_of D))) and
A16: (upper_volume (g,(division_of D))) . x = sup (rng (upper_volume (g,(division_of D)))) by FUNCT_1:def 3;
A17: dom (upper_volume (g,(division_of D))) = Seg (len (upper_volume (g,(division_of D)))) by FINSEQ_1:def 3
.= Seg (len (division_of D)) by INTEGRA1:def 6
.= dom (division_of D) by FINSEQ_1:def 3 ;
reconsider i = x as Nat by A15;
thus contradiction by A14, A15, A17, A16, A12; :: thesis: verum

end;

hence delta (division_of D) <= r ; :: thesis: verum