let A be non empty closed_interval Subset of REAL; :: thesis: for D1, MD1 being Division of A st MD1 = <*()*> ^ D1 holds
delta MD1 = delta D1

let D1, MD1 be Division of A; :: thesis: ( MD1 = <*()*> ^ D1 implies delta MD1 = delta D1 )
assume A1: MD1 = <*()*> ^ 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 ;
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 ;
A10: 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, A9, Th9; :: thesis: verum
end;
suppose j <> 1 ; :: thesis: delta MD1 <= delta D1
then not j in Seg 1 by ;
then not j in Seg () by FINSEQ_1:39;
then A11: not j in dom <*()*> by FINSEQ_1:def 3;
j in dom MD1 by ;
then consider k being Nat such that
A12: k in dom D1 and
A13: j = () + k by ;
A14: k in Seg (len D1) by ;
then divset (D1,k) = divset (MD1,(k + 1)) by
.= divset (MD1,j) by ;
then delta MD1 = (upper_bound (rng ((chi (A,A)) | (divset (D1,k))))) * (vol (divset (D1,k))) by ;
then A15: delta MD1 = (upper_volume ((chi (A,A)),D1)) . k by ;
k in Seg (len (upper_volume ((chi (A,A)),D1))) by ;
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 ;
hence delta MD1 <= delta D1 by XXREAL_2:def 8; :: thesis: verum
end;
end;
end;
i in Seg (len (upper_volume ((chi (A,A)),D1))) by ;
then A16: i in Seg (len D1) by INTEGRA1:def 6;
then i in dom D1 by FINSEQ_1:def 3;
then (len <*()*>) + i in dom MD1 by ;
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 ;
then delta D1 = (upper_bound (rng ((chi (A,A)) | (divset (D1,i))))) * (vol (divset (D1,i))) by
.= (upper_bound (rng ((chi (A,A)) | (divset (MD1,(i + 1)))))) * (vol (divset (D1,i))) by
.= (upper_bound (rng ((chi (A,A)) | (divset (MD1,(i + 1)))))) * (vol (divset (MD1,(i + 1)))) by ;
then delta D1 = (upper_volume ((chi (A,A)),MD1)) . (i + 1) by ;
then delta D1 in rng (upper_volume ((chi (A,A)),MD1)) by ;
then delta D1 <= delta MD1 by XXREAL_2:def 8;
hence delta MD1 = delta D1 by ; :: thesis: verum