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;

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

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;

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;

end;