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

for n, k being Nat st D divide_into_equal n & k in dom D holds

vol (divset (D,k)) = (vol A) / n

let D be Division of A; :: thesis: for n, k being Nat st D divide_into_equal n & k in dom D holds

vol (divset (D,k)) = (vol A) / n

let n, k be Nat; :: thesis: ( D divide_into_equal n & k in dom D implies vol (divset (D,k)) = (vol A) / n )

assume that

A1: D divide_into_equal n and

A2: k in dom D ; :: thesis: vol (divset (D,k)) = (vol A) / n

A3: len D = n by A1, INTEGRA4:def 1;

then A4: D . k = (lower_bound A) + (((vol A) / n) * k) by A1, A2, INTEGRA4:def 1;

for n, k being Nat st D divide_into_equal n & k in dom D holds

vol (divset (D,k)) = (vol A) / n

let D be Division of A; :: thesis: for n, k being Nat st D divide_into_equal n & k in dom D holds

vol (divset (D,k)) = (vol A) / n

let n, k be Nat; :: thesis: ( D divide_into_equal n & k in dom D implies vol (divset (D,k)) = (vol A) / n )

assume that

A1: D divide_into_equal n and

A2: k in dom D ; :: thesis: vol (divset (D,k)) = (vol A) / n

A3: len D = n by A1, INTEGRA4:def 1;

then A4: D . k = (lower_bound A) + (((vol A) / n) * k) by A1, A2, INTEGRA4:def 1;

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

end;

suppose A5:
k = 1
; :: thesis: vol (divset (D,k)) = (vol A) / n

then
( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = D . k )
by A2, INTEGRA1:def 4;

then vol (divset (D,k)) = (D . k) - (lower_bound A) by INTEGRA1:def 5;

hence vol (divset (D,k)) = (vol A) / n by A4, A5; :: thesis: verum

end;then vol (divset (D,k)) = (D . k) - (lower_bound A) by INTEGRA1:def 5;

hence vol (divset (D,k)) = (vol A) / n by A4, A5; :: thesis: verum

suppose A6:
k <> 1
; :: thesis: vol (divset (D,k)) = (vol A) / n

then A7:
( lower_bound (divset (D,k)) = D . (k - 1) & upper_bound (divset (D,k)) = D . k )
by A2, INTEGRA1:def 4;

A8: ( 1 <= k & k <= len D ) by A2, FINSEQ_3:25;

then A9: 1 < k by A6, XXREAL_0:1;

then reconsider j = k - 1 as Nat by NAT_1:20;

k = j + 1 ;

then ( 1 <= j & j <= k ) by A9, NAT_1:19;

then ( 1 <= j & j <= len D ) by A8, XXREAL_0:2;

then j in dom D by FINSEQ_3:25;

then A10: D . j = (lower_bound A) + (((vol A) / n) * j) by A1, A3, INTEGRA4:def 1;

vol (divset (D,k)) = (D . k) - (D . j) by A7, INTEGRA1:def 5

.= ((vol A) / n) * 1 by A4, A10 ;

hence vol (divset (D,k)) = (vol A) / n ; :: thesis: verum

end;A8: ( 1 <= k & k <= len D ) by A2, FINSEQ_3:25;

then A9: 1 < k by A6, XXREAL_0:1;

then reconsider j = k - 1 as Nat by NAT_1:20;

k = j + 1 ;

then ( 1 <= j & j <= k ) by A9, NAT_1:19;

then ( 1 <= j & j <= len D ) by A8, XXREAL_0:2;

then j in dom D by FINSEQ_3:25;

then A10: D . j = (lower_bound A) + (((vol A) / n) * j) by A1, A3, INTEGRA4:def 1;

vol (divset (D,k)) = (D . k) - (D . j) by A7, INTEGRA1:def 5

.= ((vol A) / n) * 1 by A4, A10 ;

hence vol (divset (D,k)) = (vol A) / n ; :: thesis: verum