let A be closed-interval Subset of REAL ; :: thesis: for D1, MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds
delta MD1 = delta D1
let D1, MD1 be Division of A; :: thesis: ( MD1 = <*(lower_bound A)*> ^ D1 implies delta MD1 = delta D1 )
assume A1: MD1 = <*(lower_bound A)*> ^ D1 ; :: thesis: delta MD1 = delta D1
then A2: vol (divset MD1,1) = 0 by Lm12;
A3: delta D1 = max (rng (upper_volume (chi A,A),D1)) by INTEGRA1:def 19;
then ( delta D1 in rng (upper_volume (chi A,A),D1) & ( for x being Real st x in rng (upper_volume (chi A,A),D1) holds
x <= delta D1 ) ) by XXREAL_2:def 8;
then consider i being Element of NAT such that
A4: ( i in dom (upper_volume (chi A,A),D1) & (upper_volume (chi A,A),D1) . i = delta D1 ) by PARTFUN1:26;
A5: delta MD1 = max (rng (upper_volume (chi A,A),MD1)) by INTEGRA1:def 19;
then ( delta MD1 in rng (upper_volume (chi A,A),MD1) & ( for x being Real st x in rng (upper_volume (chi A,A),MD1) holds
x <= delta MD1 ) ) by XXREAL_2:def 8;
then consider j being Element of NAT such that
A6: ( j in dom (upper_volume (chi A,A),MD1) & (upper_volume (chi A,A),MD1) . j = delta MD1 ) by PARTFUN1:26;
i in Seg (len (upper_volume (chi A,A),D1)) by A4, FINSEQ_1:def 3;
then A7: i in Seg (len D1) by INTEGRA1:def 7;
then i in dom D1 by FINSEQ_1:def 3;
then A8: delta D1 = (upper_bound (rng ((chi A,A) | (divset D1,i)))) * (vol (divset D1,i)) by A4, INTEGRA1:def 7
.= (upper_bound (rng ((chi A,A) | (divset MD1,(i + 1))))) * (vol (divset D1,i)) by A1, A7, Lm11
.= (upper_bound (rng ((chi A,A) | (divset MD1,(i + 1))))) * (vol (divset MD1,(i + 1))) by A1, A7, Lm11 ;
i in dom D1 by A7, FINSEQ_1:def 3;
then (len <*(lower_bound A)*>) + i in dom MD1 by A1, FINSEQ_1:41;
then i + 1 in dom MD1 by FINSEQ_1:56;
then A9: i + 1 in Seg (len MD1) by FINSEQ_1:def 3;
then i + 1 in dom MD1 by FINSEQ_1:def 3;
then A10: delta D1 = (upper_volume (chi A,A),MD1) . (i + 1) by A8, INTEGRA1:def 7;
i + 1 in Seg (len (upper_volume (chi A,A),MD1)) by A9, INTEGRA1:def 7;
then i + 1 in dom (upper_volume (chi A,A),MD1) by FINSEQ_1:def 3;
then delta D1 in rng (upper_volume (chi A,A),MD1) by A10, FUNCT_1:def 5;
then A11: delta D1 <= delta MD1 by A5, XXREAL_2:def 8;
j in Seg (len (upper_volume (chi A,A),MD1)) by A6, FINSEQ_1:def 3;
then A12: j in Seg (len MD1) by INTEGRA1:def 7;
then B12: j in dom MD1 by FINSEQ_1:def 3;
then A13: delta MD1 = (upper_bound (rng ((chi A,A) | (divset MD1,j)))) * (vol (divset MD1,j)) by A6, INTEGRA1:def 7;
delta MD1 <= delta D1

proof

per cases ( j = 1 or j <> 1 ) ;

suppose j = 1 ; :: thesis: delta MD1 <= delta D1

hence delta MD1 <= delta D1 by A2, A13, Th8; :: thesis: verum

end;

suppose j <> 1 ; :: thesis: delta MD1 <= delta D1

then not j in Seg 1 by FINSEQ_1:4, TARSKI:def 1;
then not j in Seg (len <*(lower_bound A)*>) by FINSEQ_1:56;
then A14: not j in dom <*(lower_bound A)*> by FINSEQ_1:def 3;
j in dom MD1 by A12, FINSEQ_1:def 3;
then consider k being Nat such that
A15: ( k in dom D1 & j = (len <*(lower_bound A)*>) + k ) by A1, A14, FINSEQ_1:38;
A16: k in Seg (len D1) by A15, FINSEQ_1:def 3;
then B16: k in dom D1 by FINSEQ_1:def 3;
divset D1,k = divset MD1,(k + 1) by A1, Lm11, A16
.= divset MD1,j by A15, FINSEQ_1:56 ;
then delta MD1 = (upper_bound (rng ((chi A,A) | (divset D1,k)))) * (vol (divset D1,k)) by A6, B12, INTEGRA1:def 7;
then A17: delta MD1 = (upper_volume (chi A,A),D1) . k by B16, INTEGRA1:def 7;
k in Seg (len (upper_volume (chi A,A),D1)) by A16, INTEGRA1:def 7;
then k in dom (upper_volume (chi A,A),D1) by FINSEQ_1:def 3;
then delta MD1 in rng (upper_volume (chi A,A),D1) by A17, FUNCT_1:def 5;
hence delta MD1 <= delta D1 by A3, XXREAL_2:def 8; :: thesis: verum

end;

end;

end;

hence delta MD1 = delta D1 by A11, XXREAL_0:1; :: thesis: verum