let A be non empty closed_interval Subset of REAL; :: thesis: for D1 being Division of A

for f being Function of A,REAL

for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds

( ( for i being Element of NAT st i in Seg (len D1) holds

divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )

let D1 be Division of A; :: thesis: for f being Function of A,REAL

for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds

( ( for i being Element of NAT st i in Seg (len D1) holds

divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )

let f be Function of A,REAL; :: thesis: for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds

( ( for i being Element of NAT st i in Seg (len D1) holds

divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )

let MD1 be Division of A; :: thesis: ( MD1 = <*(lower_bound A)*> ^ D1 implies ( ( for i being Element of NAT st i in Seg (len D1) holds

divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 ) )

assume A1: MD1 = <*(lower_bound A)*> ^ D1 ; :: thesis: ( ( for i being Element of NAT st i in Seg (len D1) holds

divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )

thus A2: for i being Element of NAT st i in Seg (len D1) holds

divset (MD1,(i + 1)) = divset (D1,i) :: thesis: ( upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )

.= 1 + (len D1) by FINSEQ_1:39 ;

thus upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 :: thesis: lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1

then 1 in dom (lower_volume (f,MD1)) by FINSEQ_3:32;

then 1 <= len (lower_volume (f,MD1)) by FINSEQ_3:25;

then len ((lower_volume (f,MD1)) /^ 1) = (len (lower_volume (f,MD1))) - 1 by RFINSEQ:def 1

.= (len MD1) - 1 by INTEGRA1:def 7

.= len D1 by A16 ;

then A26: len (lower_volume (f,D1)) = len ((lower_volume (f,MD1)) /^ 1) by INTEGRA1:def 7;

for k being Nat st 1 <= k & k <= len (lower_volume (f,D1)) holds

(lower_volume (f,D1)) . k = ((lower_volume (f,MD1)) /^ 1) . k

for f being Function of A,REAL

for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds

( ( for i being Element of NAT st i in Seg (len D1) holds

divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )

let D1 be Division of A; :: thesis: for f being Function of A,REAL

for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds

( ( for i being Element of NAT st i in Seg (len D1) holds

divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )

let f be Function of A,REAL; :: thesis: for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds

( ( for i being Element of NAT st i in Seg (len D1) holds

divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )

let MD1 be Division of A; :: thesis: ( MD1 = <*(lower_bound A)*> ^ D1 implies ( ( for i being Element of NAT st i in Seg (len D1) holds

divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 ) )

assume A1: MD1 = <*(lower_bound A)*> ^ D1 ; :: thesis: ( ( for i being Element of NAT st i in Seg (len D1) holds

divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )

thus A2: for i being Element of NAT st i in Seg (len D1) holds

divset (MD1,(i + 1)) = divset (D1,i) :: thesis: ( upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )

proof

A16: len MD1 =
(len <*(lower_bound A)*>) + (len D1)
by A1, FINSEQ_1:22
let i be Element of NAT ; :: thesis: ( i in Seg (len D1) implies divset (MD1,(i + 1)) = divset (D1,i) )

assume A3: i in Seg (len D1) ; :: thesis: divset (MD1,(i + 1)) = divset (D1,i)

then A4: i in dom D1 by FINSEQ_1:def 3;

i <= len D1 by A3, FINSEQ_1:1;

then i + 1 <= (len D1) + 1 by XREAL_1:6;

then i + 1 <= (len D1) + (len <*(lower_bound A)*>) by FINSEQ_1:39;

then A5: i + 1 <= len MD1 by A1, FINSEQ_1:22;

1 <= i + 1 by NAT_1:11;

then A6: i + 1 in dom MD1 by A5, FINSEQ_3:25;

A7: 1 <= i by A3, FINSEQ_1:1;

A8: ( lower_bound (divset (D1,i)) = lower_bound (divset (MD1,(i + 1))) & upper_bound (divset (D1,i)) = upper_bound (divset (MD1,(i + 1))) )

hence divset (MD1,(i + 1)) = divset (D1,i) by A8, INTEGRA1:4; :: thesis: verum

end;assume A3: i in Seg (len D1) ; :: thesis: divset (MD1,(i + 1)) = divset (D1,i)

then A4: i in dom D1 by FINSEQ_1:def 3;

i <= len D1 by A3, FINSEQ_1:1;

then i + 1 <= (len D1) + 1 by XREAL_1:6;

then i + 1 <= (len D1) + (len <*(lower_bound A)*>) by FINSEQ_1:39;

then A5: i + 1 <= len MD1 by A1, FINSEQ_1:22;

1 <= i + 1 by NAT_1:11;

then A6: i + 1 in dom MD1 by A5, FINSEQ_3:25;

A7: 1 <= i by A3, FINSEQ_1:1;

A8: ( lower_bound (divset (D1,i)) = lower_bound (divset (MD1,(i + 1))) & upper_bound (divset (D1,i)) = upper_bound (divset (MD1,(i + 1))) )

proof
end;

divset (D1,i) = [.(lower_bound (divset (D1,i))),(upper_bound (divset (D1,i))).]
by INTEGRA1:4;per cases
( i = 1 or i <> 1 )
;

end;

suppose A9:
i = 1
; :: thesis: ( lower_bound (divset (D1,i)) = lower_bound (divset (MD1,(i + 1))) & upper_bound (divset (D1,i)) = upper_bound (divset (MD1,(i + 1))) )

A10:
i + 1 > 1
by A7, NAT_1:13;

then lower_bound (divset (MD1,(i + 1))) = MD1 . ((i + 1) - 1) by A6, INTEGRA1:def 4;

then A11: lower_bound (divset (MD1,(i + 1))) = lower_bound A by A1, A9, FINSEQ_1:41;

A12: MD1 . (i + 1) = MD1 . (i + (len <*(lower_bound A)*>)) by FINSEQ_1:40

.= D1 . i by A1, A4, FINSEQ_1:def 7 ;

upper_bound (divset (MD1,(i + 1))) = MD1 . (i + 1) by A6, A10, INTEGRA1:def 4;

hence ( lower_bound (divset (D1,i)) = lower_bound (divset (MD1,(i + 1))) & upper_bound (divset (D1,i)) = upper_bound (divset (MD1,(i + 1))) ) by A4, A9, A11, A12, INTEGRA1:def 4; :: thesis: verum

end;then lower_bound (divset (MD1,(i + 1))) = MD1 . ((i + 1) - 1) by A6, INTEGRA1:def 4;

then A11: lower_bound (divset (MD1,(i + 1))) = lower_bound A by A1, A9, FINSEQ_1:41;

A12: MD1 . (i + 1) = MD1 . (i + (len <*(lower_bound A)*>)) by FINSEQ_1:40

.= D1 . i by A1, A4, FINSEQ_1:def 7 ;

upper_bound (divset (MD1,(i + 1))) = MD1 . (i + 1) by A6, A10, INTEGRA1:def 4;

hence ( lower_bound (divset (D1,i)) = lower_bound (divset (MD1,(i + 1))) & upper_bound (divset (D1,i)) = upper_bound (divset (MD1,(i + 1))) ) by A4, A9, A11, A12, INTEGRA1:def 4; :: thesis: verum

suppose A13:
i <> 1
; :: thesis: ( lower_bound (divset (D1,i)) = lower_bound (divset (MD1,(i + 1))) & upper_bound (divset (D1,i)) = upper_bound (divset (MD1,(i + 1))) )

A14:
i + 1 > 1
by A7, NAT_1:13;

MD1 . (i + 1) = MD1 . (i + (len <*(lower_bound A)*>)) by FINSEQ_1:40

.= D1 . i by A1, A4, FINSEQ_1:def 7 ;

then A15: upper_bound (divset (MD1,(i + 1))) = D1 . i by A6, A14, INTEGRA1:def 4

.= upper_bound (divset (D1,i)) by A4, A13, INTEGRA1:def 4 ;

i - 1 in dom D1 by A4, A13, INTEGRA1:7;

then D1 . (i - 1) = MD1 . ((i - 1) + (len <*(lower_bound A)*>)) by A1, FINSEQ_1:def 7

.= MD1 . ((i - 1) + 1) by FINSEQ_1:39

.= MD1 . ((i + 1) - 1) ;

then lower_bound (divset (D1,i)) = MD1 . ((i + 1) - 1) by A4, A13, INTEGRA1:def 4

.= lower_bound (divset (MD1,(i + 1))) by A6, A14, INTEGRA1:def 4 ;

hence ( lower_bound (divset (D1,i)) = lower_bound (divset (MD1,(i + 1))) & upper_bound (divset (D1,i)) = upper_bound (divset (MD1,(i + 1))) ) by A15; :: thesis: verum

end;MD1 . (i + 1) = MD1 . (i + (len <*(lower_bound A)*>)) by FINSEQ_1:40

.= D1 . i by A1, A4, FINSEQ_1:def 7 ;

then A15: upper_bound (divset (MD1,(i + 1))) = D1 . i by A6, A14, INTEGRA1:def 4

.= upper_bound (divset (D1,i)) by A4, A13, INTEGRA1:def 4 ;

i - 1 in dom D1 by A4, A13, INTEGRA1:7;

then D1 . (i - 1) = MD1 . ((i - 1) + (len <*(lower_bound A)*>)) by A1, FINSEQ_1:def 7

.= MD1 . ((i - 1) + 1) by FINSEQ_1:39

.= MD1 . ((i + 1) - 1) ;

then lower_bound (divset (D1,i)) = MD1 . ((i + 1) - 1) by A4, A13, INTEGRA1:def 4

.= lower_bound (divset (MD1,(i + 1))) by A6, A14, INTEGRA1:def 4 ;

hence ( lower_bound (divset (D1,i)) = lower_bound (divset (MD1,(i + 1))) & upper_bound (divset (D1,i)) = upper_bound (divset (MD1,(i + 1))) ) by A15; :: thesis: verum

hence divset (MD1,(i + 1)) = divset (D1,i) by A8, INTEGRA1:4; :: thesis: verum

.= 1 + (len D1) by FINSEQ_1:39 ;

thus upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 :: thesis: lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1

proof

rng (lower_volume (f,MD1)) <> {}
;
set D2 = D1;

set MD2 = MD1;

rng (upper_volume (f,MD1)) <> {} ;

then 1 in dom (upper_volume (f,MD1)) by FINSEQ_3:32;

then 1 <= len (upper_volume (f,MD1)) by FINSEQ_3:25;

then len ((upper_volume (f,MD1)) /^ 1) = (len (upper_volume (f,MD1))) - 1 by RFINSEQ:def 1

.= (len MD1) - 1 by INTEGRA1:def 6

.= len D1 by A16 ;

then A17: len (upper_volume (f,D1)) = len ((upper_volume (f,MD1)) /^ 1) by INTEGRA1:def 6;

for k being Nat st 1 <= k & k <= len (upper_volume (f,D1)) holds

(upper_volume (f,D1)) . k = ((upper_volume (f,MD1)) /^ 1) . k

end;set MD2 = MD1;

rng (upper_volume (f,MD1)) <> {} ;

then 1 in dom (upper_volume (f,MD1)) by FINSEQ_3:32;

then 1 <= len (upper_volume (f,MD1)) by FINSEQ_3:25;

then len ((upper_volume (f,MD1)) /^ 1) = (len (upper_volume (f,MD1))) - 1 by RFINSEQ:def 1

.= (len MD1) - 1 by INTEGRA1:def 6

.= len D1 by A16 ;

then A17: len (upper_volume (f,D1)) = len ((upper_volume (f,MD1)) /^ 1) by INTEGRA1:def 6;

for k being Nat st 1 <= k & k <= len (upper_volume (f,D1)) holds

(upper_volume (f,D1)) . k = ((upper_volume (f,MD1)) /^ 1) . k

proof

hence
upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1
by A17, FINSEQ_1:14; :: thesis: verum
let k be Nat; :: thesis: ( 1 <= k & k <= len (upper_volume (f,D1)) implies (upper_volume (f,D1)) . k = ((upper_volume (f,MD1)) /^ 1) . k )

assume that

A18: 1 <= k and

A19: k <= len (upper_volume (f,D1)) ; :: thesis: (upper_volume (f,D1)) . k = ((upper_volume (f,MD1)) /^ 1) . k

k + 1 <= (len (upper_volume (f,D1))) + 1 by A19, XREAL_1:6;

then A20: k + 1 <= (len D1) + 1 by INTEGRA1:def 6;

k in Seg (len (upper_volume (f,D1))) by A18, A19, FINSEQ_1:1;

then A21: k in Seg (len D1) by INTEGRA1:def 6;

then k in dom D1 by FINSEQ_1:def 3;

then A22: (upper_volume (f,D1)) . k = (upper_bound (rng (f | (divset (D1,k))))) * (vol (divset (D1,k))) by INTEGRA1:def 6

.= (upper_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (D1,k))) by A2, A21

.= (upper_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (MD1,(k + 1)))) by A2, A21 ;

A23: len ((upper_volume (f,MD1)) /^ 1) <= len (upper_volume (f,MD1)) by FINSEQ_5:25;

1 <= k + 1 by NAT_1:11;

then k + 1 in Seg (len MD1) by A16, A20, FINSEQ_1:1;

then A24: k + 1 in dom MD1 by FINSEQ_1:def 3;

1 <= len (upper_volume (f,D1)) by A18, A19, XXREAL_0:2;

then A25: 1 <= len (upper_volume (f,MD1)) by A17, A23, XXREAL_0:2;

k in dom ((upper_volume (f,MD1)) /^ 1) by A17, A18, A19, FINSEQ_3:25;

then ((upper_volume (f,MD1)) /^ 1) . k = (upper_volume (f,MD1)) . (k + 1) by A25, RFINSEQ:def 1

.= (upper_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (MD1,(k + 1)))) by A24, INTEGRA1:def 6 ;

hence (upper_volume (f,D1)) . k = ((upper_volume (f,MD1)) /^ 1) . k by A22; :: thesis: verum

end;assume that

A18: 1 <= k and

A19: k <= len (upper_volume (f,D1)) ; :: thesis: (upper_volume (f,D1)) . k = ((upper_volume (f,MD1)) /^ 1) . k

k + 1 <= (len (upper_volume (f,D1))) + 1 by A19, XREAL_1:6;

then A20: k + 1 <= (len D1) + 1 by INTEGRA1:def 6;

k in Seg (len (upper_volume (f,D1))) by A18, A19, FINSEQ_1:1;

then A21: k in Seg (len D1) by INTEGRA1:def 6;

then k in dom D1 by FINSEQ_1:def 3;

then A22: (upper_volume (f,D1)) . k = (upper_bound (rng (f | (divset (D1,k))))) * (vol (divset (D1,k))) by INTEGRA1:def 6

.= (upper_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (D1,k))) by A2, A21

.= (upper_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (MD1,(k + 1)))) by A2, A21 ;

A23: len ((upper_volume (f,MD1)) /^ 1) <= len (upper_volume (f,MD1)) by FINSEQ_5:25;

1 <= k + 1 by NAT_1:11;

then k + 1 in Seg (len MD1) by A16, A20, FINSEQ_1:1;

then A24: k + 1 in dom MD1 by FINSEQ_1:def 3;

1 <= len (upper_volume (f,D1)) by A18, A19, XXREAL_0:2;

then A25: 1 <= len (upper_volume (f,MD1)) by A17, A23, XXREAL_0:2;

k in dom ((upper_volume (f,MD1)) /^ 1) by A17, A18, A19, FINSEQ_3:25;

then ((upper_volume (f,MD1)) /^ 1) . k = (upper_volume (f,MD1)) . (k + 1) by A25, RFINSEQ:def 1

.= (upper_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (MD1,(k + 1)))) by A24, INTEGRA1:def 6 ;

hence (upper_volume (f,D1)) . k = ((upper_volume (f,MD1)) /^ 1) . k by A22; :: thesis: verum

then 1 in dom (lower_volume (f,MD1)) by FINSEQ_3:32;

then 1 <= len (lower_volume (f,MD1)) by FINSEQ_3:25;

then len ((lower_volume (f,MD1)) /^ 1) = (len (lower_volume (f,MD1))) - 1 by RFINSEQ:def 1

.= (len MD1) - 1 by INTEGRA1:def 7

.= len D1 by A16 ;

then A26: len (lower_volume (f,D1)) = len ((lower_volume (f,MD1)) /^ 1) by INTEGRA1:def 7;

for k being Nat st 1 <= k & k <= len (lower_volume (f,D1)) holds

(lower_volume (f,D1)) . k = ((lower_volume (f,MD1)) /^ 1) . k

proof

hence
lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1
by A26, FINSEQ_1:14; :: thesis: verum
let k be Nat; :: thesis: ( 1 <= k & k <= len (lower_volume (f,D1)) implies (lower_volume (f,D1)) . k = ((lower_volume (f,MD1)) /^ 1) . k )

assume that

A27: 1 <= k and

A28: k <= len (lower_volume (f,D1)) ; :: thesis: (lower_volume (f,D1)) . k = ((lower_volume (f,MD1)) /^ 1) . k

A29: 1 <= k + 1 by NAT_1:11;

k in Seg (len (lower_volume (f,D1))) by A27, A28, FINSEQ_1:1;

then A30: k in Seg (len D1) by INTEGRA1:def 7;

then k in dom D1 by FINSEQ_1:def 3;

then A31: (lower_volume (f,D1)) . k = (lower_bound (rng (f | (divset (D1,k))))) * (vol (divset (D1,k))) by INTEGRA1:def 7

.= (lower_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (D1,k))) by A2, A30

.= (lower_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (MD1,(k + 1)))) by A2, A30 ;

A32: len ((lower_volume (f,MD1)) /^ 1) <= len (lower_volume (f,MD1)) by FINSEQ_5:25;

k + 1 <= (len (lower_volume (f,D1))) + 1 by A28, XREAL_1:6;

then A33: k + 1 <= (len D1) + 1 by INTEGRA1:def 7;

len MD1 = (len <*(lower_bound A)*>) + (len D1) by A1, FINSEQ_1:22

.= (len D1) + 1 by FINSEQ_1:39 ;

then k + 1 in Seg (len MD1) by A29, A33, FINSEQ_1:1;

then A34: k + 1 in dom MD1 by FINSEQ_1:def 3;

1 <= len ((lower_volume (f,MD1)) /^ 1) by A26, A27, A28, XXREAL_0:2;

then A35: 1 <= len (lower_volume (f,MD1)) by A32, XXREAL_0:2;

k in dom ((lower_volume (f,MD1)) /^ 1) by A26, A27, A28, FINSEQ_3:25;

then ((lower_volume (f,MD1)) /^ 1) . k = (lower_volume (f,MD1)) . (k + 1) by A35, RFINSEQ:def 1

.= (lower_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (MD1,(k + 1)))) by A34, INTEGRA1:def 7 ;

hence (lower_volume (f,D1)) . k = ((lower_volume (f,MD1)) /^ 1) . k by A31; :: thesis: verum

end;assume that

A27: 1 <= k and

A28: k <= len (lower_volume (f,D1)) ; :: thesis: (lower_volume (f,D1)) . k = ((lower_volume (f,MD1)) /^ 1) . k

A29: 1 <= k + 1 by NAT_1:11;

k in Seg (len (lower_volume (f,D1))) by A27, A28, FINSEQ_1:1;

then A30: k in Seg (len D1) by INTEGRA1:def 7;

then k in dom D1 by FINSEQ_1:def 3;

then A31: (lower_volume (f,D1)) . k = (lower_bound (rng (f | (divset (D1,k))))) * (vol (divset (D1,k))) by INTEGRA1:def 7

.= (lower_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (D1,k))) by A2, A30

.= (lower_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (MD1,(k + 1)))) by A2, A30 ;

A32: len ((lower_volume (f,MD1)) /^ 1) <= len (lower_volume (f,MD1)) by FINSEQ_5:25;

k + 1 <= (len (lower_volume (f,D1))) + 1 by A28, XREAL_1:6;

then A33: k + 1 <= (len D1) + 1 by INTEGRA1:def 7;

len MD1 = (len <*(lower_bound A)*>) + (len D1) by A1, FINSEQ_1:22

.= (len D1) + 1 by FINSEQ_1:39 ;

then k + 1 in Seg (len MD1) by A29, A33, FINSEQ_1:1;

then A34: k + 1 in dom MD1 by FINSEQ_1:def 3;

1 <= len ((lower_volume (f,MD1)) /^ 1) by A26, A27, A28, XXREAL_0:2;

then A35: 1 <= len (lower_volume (f,MD1)) by A32, XXREAL_0:2;

k in dom ((lower_volume (f,MD1)) /^ 1) by A26, A27, A28, FINSEQ_3:25;

then ((lower_volume (f,MD1)) /^ 1) . k = (lower_volume (f,MD1)) . (k + 1) by A35, RFINSEQ:def 1

.= (lower_bound (rng (f | (divset (MD1,(k + 1)))))) * (vol (divset (MD1,(k + 1)))) by A34, INTEGRA1:def 7 ;

hence (lower_volume (f,D1)) . k = ((lower_volume (f,MD1)) /^ 1) . k by A31; :: thesis: verum