let A be non empty 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 Lm11;

delta D1 in rng (upper_volume ((chi (A,A)),D1)) by XXREAL_2:def 8;

then consider i being Element of NAT such that

A3: i in dom (upper_volume ((chi (A,A)),D1)) and

A4: (upper_volume ((chi (A,A)),D1)) . i = delta D1 by PARTFUN1:3;

delta MD1 in rng (upper_volume ((chi (A,A)),MD1)) by XXREAL_2:def 8;

then consider j being Element of NAT such that

A5: j in dom (upper_volume ((chi (A,A)),MD1)) and

A6: (upper_volume ((chi (A,A)),MD1)) . j = delta MD1 by PARTFUN1:3;

j in Seg (len (upper_volume ((chi (A,A)),MD1))) by A5, FINSEQ_1:def 3;

then A7: j in Seg (len MD1) by INTEGRA1:def 6;

then A8: j in dom MD1 by FINSEQ_1:def 3;

then A9: delta MD1 = (upper_bound (rng ((chi (A,A)) | (divset (MD1,j))))) * (vol (divset (MD1,j))) by A6, INTEGRA1:def 6;

A10: delta MD1 <= delta D1

then A16: i in Seg (len D1) by INTEGRA1:def 6;

then i in dom D1 by FINSEQ_1:def 3;

then (len <*(lower_bound A)*>) + i in dom MD1 by A1, FINSEQ_1:28;

then A17: i + 1 in dom MD1 by FINSEQ_1:39;

then i + 1 in Seg (len MD1) by FINSEQ_1:def 3;

then i + 1 in Seg (len (upper_volume ((chi (A,A)),MD1))) by INTEGRA1:def 6;

then A18: i + 1 in dom (upper_volume ((chi (A,A)),MD1)) by FINSEQ_1:def 3;

i in dom D1 by A16, FINSEQ_1:def 3;

then delta D1 = (upper_bound (rng ((chi (A,A)) | (divset (D1,i))))) * (vol (divset (D1,i))) by A4, INTEGRA1:def 6

.= (upper_bound (rng ((chi (A,A)) | (divset (MD1,(i + 1)))))) * (vol (divset (D1,i))) by A1, A16, Lm10

.= (upper_bound (rng ((chi (A,A)) | (divset (MD1,(i + 1)))))) * (vol (divset (MD1,(i + 1)))) by A1, A16, Lm10 ;

then delta D1 = (upper_volume ((chi (A,A)),MD1)) . (i + 1) by A17, INTEGRA1:def 6;

then delta D1 in rng (upper_volume ((chi (A,A)),MD1)) by A18, FUNCT_1:def 3;

then delta D1 <= delta MD1 by XXREAL_2:def 8;

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

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 Lm11;

delta D1 in rng (upper_volume ((chi (A,A)),D1)) by XXREAL_2:def 8;

then consider i being Element of NAT such that

A3: i in dom (upper_volume ((chi (A,A)),D1)) and

A4: (upper_volume ((chi (A,A)),D1)) . i = delta D1 by PARTFUN1:3;

delta MD1 in rng (upper_volume ((chi (A,A)),MD1)) by XXREAL_2:def 8;

then consider j being Element of NAT such that

A5: j in dom (upper_volume ((chi (A,A)),MD1)) and

A6: (upper_volume ((chi (A,A)),MD1)) . j = delta MD1 by PARTFUN1:3;

j in Seg (len (upper_volume ((chi (A,A)),MD1))) by A5, FINSEQ_1:def 3;

then A7: j in Seg (len MD1) by INTEGRA1:def 6;

then A8: j in dom MD1 by FINSEQ_1:def 3;

then A9: delta MD1 = (upper_bound (rng ((chi (A,A)) | (divset (MD1,j))))) * (vol (divset (MD1,j))) by A6, INTEGRA1:def 6;

A10: delta MD1 <= delta D1

proof
end;

i in Seg (len (upper_volume ((chi (A,A)),D1)))
by A3, FINSEQ_1:def 3;per cases
( j = 1 or j <> 1 )
;

end;

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

then
not j in Seg 1
by FINSEQ_1:2, TARSKI:def 1;

then not j in Seg (len <*(lower_bound A)*>) by FINSEQ_1:39;

then A11: not j in dom <*(lower_bound A)*> by FINSEQ_1:def 3;

j in dom MD1 by A7, FINSEQ_1:def 3;

then consider k being Nat such that

A12: k in dom D1 and

A13: j = (len <*(lower_bound A)*>) + k by A1, A11, FINSEQ_1:25;

A14: k in Seg (len D1) by A12, FINSEQ_1:def 3;

then divset (D1,k) = divset (MD1,(k + 1)) by A1, Lm10

.= divset (MD1,j) by A13, FINSEQ_1:39 ;

then delta MD1 = (upper_bound (rng ((chi (A,A)) | (divset (D1,k))))) * (vol (divset (D1,k))) by A6, A8, INTEGRA1:def 6;

then A15: delta MD1 = (upper_volume ((chi (A,A)),D1)) . k by A12, INTEGRA1:def 6;

k in Seg (len (upper_volume ((chi (A,A)),D1))) by A14, INTEGRA1:def 6;

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 A15, FUNCT_1:def 3;

hence delta MD1 <= delta D1 by XXREAL_2:def 8; :: thesis: verum

end;then not j in Seg (len <*(lower_bound A)*>) by FINSEQ_1:39;

then A11: not j in dom <*(lower_bound A)*> by FINSEQ_1:def 3;

j in dom MD1 by A7, FINSEQ_1:def 3;

then consider k being Nat such that

A12: k in dom D1 and

A13: j = (len <*(lower_bound A)*>) + k by A1, A11, FINSEQ_1:25;

A14: k in Seg (len D1) by A12, FINSEQ_1:def 3;

then divset (D1,k) = divset (MD1,(k + 1)) by A1, Lm10

.= divset (MD1,j) by A13, FINSEQ_1:39 ;

then delta MD1 = (upper_bound (rng ((chi (A,A)) | (divset (D1,k))))) * (vol (divset (D1,k))) by A6, A8, INTEGRA1:def 6;

then A15: delta MD1 = (upper_volume ((chi (A,A)),D1)) . k by A12, INTEGRA1:def 6;

k in Seg (len (upper_volume ((chi (A,A)),D1))) by A14, INTEGRA1:def 6;

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 A15, FUNCT_1:def 3;

hence delta MD1 <= delta D1 by XXREAL_2:def 8; :: thesis: verum

then A16: i in Seg (len D1) by INTEGRA1:def 6;

then i in dom D1 by FINSEQ_1:def 3;

then (len <*(lower_bound A)*>) + i in dom MD1 by A1, FINSEQ_1:28;

then A17: i + 1 in dom MD1 by FINSEQ_1:39;

then i + 1 in Seg (len MD1) by FINSEQ_1:def 3;

then i + 1 in Seg (len (upper_volume ((chi (A,A)),MD1))) by INTEGRA1:def 6;

then A18: i + 1 in dom (upper_volume ((chi (A,A)),MD1)) by FINSEQ_1:def 3;

i in dom D1 by A16, FINSEQ_1:def 3;

then delta D1 = (upper_bound (rng ((chi (A,A)) | (divset (D1,i))))) * (vol (divset (D1,i))) by A4, INTEGRA1:def 6

.= (upper_bound (rng ((chi (A,A)) | (divset (MD1,(i + 1)))))) * (vol (divset (D1,i))) by A1, A16, Lm10

.= (upper_bound (rng ((chi (A,A)) | (divset (MD1,(i + 1)))))) * (vol (divset (MD1,(i + 1)))) by A1, A16, Lm10 ;

then delta D1 = (upper_volume ((chi (A,A)),MD1)) . (i + 1) by A17, INTEGRA1:def 6;

then delta D1 in rng (upper_volume ((chi (A,A)),MD1)) by A18, FUNCT_1:def 3;

then delta D1 <= delta MD1 by XXREAL_2:def 8;

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