defpred S₁[ Nat] means for A being non empty closed_interval Subset of REAL
for D being Division of A
for B being non empty closed_interval Subset of REAL
for v being FinSequence of REAL st $1 = len D & B c= A & len D = len v & ( for k being Nat st k in dom v holds
v . k = xvol (B /\ (divset (D,k))) ) holds
Sum v = vol B;
A1: S₁[ 0 ] ;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[i + 1]
let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A
for B being non empty closed_interval Subset of REAL
for v being FinSequence of REAL st i + 1 = len D & B c= A & len D = len v & ( for k being Nat st k in dom v holds
v . k = xvol (B /\ (divset (D,k))) ) holds
Sum v = vol B
let D be Division of A; :: thesis: for B being non empty closed_interval Subset of REAL
for v being FinSequence of REAL st i + 1 = len D & B c= A & len D = len v & ( for k being Nat st k in dom v holds
v . k = xvol (B /\ (divset (D,k))) ) holds
Sum v = vol B
let B be non empty closed_interval Subset of REAL; :: thesis: for v being FinSequence of REAL st i + 1 = len D & B c= A & len D = len v & ( for k being Nat st k in dom v holds
v . k = xvol (B /\ (divset (D,k))) ) holds
Sum v = vol B
let v be FinSequence of REAL ; :: thesis: ( i + 1 = len D & B c= A & len D = len v & ( for k being Nat st k in dom v holds
v . k = xvol (B /\ (divset (D,k))) ) implies Sum v = vol B )
set D1 = D | i;
set v1 = v | i;
assume A4: ( i + 1 = len D & B c= A & len D = len v & ( for k being Nat st k in dom v holds
v . k = xvol (B /\ (divset (D,k))) ) ) ; :: thesis: Sum v = vol B
A5: ( dom D = Seg (i + 1) & dom D = dom v ) by A4, FINSEQ_1:def 3, FINSEQ_3:29;
then A6: v . (i + 1) = xvol (B /\ (divset (D,(i + 1)))) by A4, FINSEQ_1:4;
A7: ( 1 <= i + 1 & i + 1 <= len v ) by A4, NAT_1:11;
v = (v | i) ^ <*(v /. (i + 1))*> by A4, FINSEQ_5:21;
then A8: v = (v | i) ^ <*(v . (i + 1))*> by A7, FINSEQ_4:15;
A9: ( lower_bound A <= lower_bound B & upper_bound B <= upper_bound A ) by A4, SEQ_4:47, SEQ_4:48;
A10: rng D c= A by INTEGRA1:def 2;
A11: rng (D | i) c= rng D by RELAT_1:70;
A12: Seg i c= dom D by A5, FINSEQ_1:5, NAT_1:11;
A13: ( i = len (D | i) & i = len (v | i) ) by FINSEQ_1:59, A4, NAT_1:11;
then A14: dom (v | i) = Seg i by FINSEQ_1:def 3;

per cases ( i <> 0 or i = 0 ) ;

suppose A15: i <> 0 ; :: thesis: Sum v = vol B

then A16: i in dom D by A12, FINSEQ_1:3;
then consider A1, A2 being non empty closed_interval Subset of REAL such that
A17: ( A1 = [.(lower_bound A),(D . i).] & A2 = [.(D . i),(upper_bound A).] & A = A1 \/ A2 ) by INTEGRA1:32;
for y being object st y in rng (D | i) holds
y in A1

proof

let y be object ; :: thesis: ( y in rng (D | i) implies y in A1 )
assume A18: y in rng (D | i) ; :: thesis: y in A1
then y in A by A11, A10;
then y in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then consider y1 being Real such that
A19: ( y = y1 & lower_bound A <= y1 & y1 <= upper_bound A ) ;
consider x being object such that
A20: ( x in dom (D | i) & y1 = (D | i) . x ) by A18, A19, FUNCT_1:def 3;
reconsider x = x as Nat by A20;
A21: x in Seg i by A13, FINSEQ_1:def 3, A20;
then A22: x <= i by FINSEQ_1:1;

now :: thesis: ( x <> i implies D . x <= D . i )

assume x <> i ; :: thesis: D . x <= D . i
then x < i by A22, XXREAL_0:1;
hence D . x <= D . i by A16, A12, A21, VALUED_0:def 13; :: thesis: verum

end;

then y1 <= D . i by A20, A21, FUNCT_1:49;
hence y in A1 by A19, A17; :: thesis: verum

end;

then A23: rng (D | i) c= A1 ;
A24: (D | i) . i = D . i by A15, FINSEQ_1:3, FUNCT_1:49;
reconsider D1 = D | i as non empty increasing FinSequence of REAL by A15;
A27: A1 = [.(lower_bound A1),(upper_bound A1).] by INTEGRA1:4;
then D1 . (len D1) = upper_bound A1 by A13, A24, A17, INTEGRA1:5;
then reconsider D1 = D1 as Division of A1 by A23, INTEGRA1:def 2;
A28: 1 < i + 1 by A15, NAT_1:16;
i + 1 in dom D by A5, FINSEQ_1:4;
then A29: ( lower_bound (divset (D,(i + 1))) = D . ((i + 1) - 1) & upper_bound (divset (D,(i + 1))) = D . (i + 1) ) by A28, INTEGRA1:def 4;
then A30: ( B = [.(lower_bound B),(upper_bound B).] & divset (D,(i + 1)) = [.(D . i),(D . (i + 1)).] ) by INTEGRA1:4;
A31: D . i <= D . (i + 1) by A29, SEQ_4:11;

per cases ( upper_bound B <= D . i or D . i < upper_bound B ) ;

suppose A32: upper_bound B <= D . i ; :: thesis: Sum v = vol B

then [.(lower_bound B),(upper_bound B).] c= [.(lower_bound A),(D . i).] by A9, XXREAL_1:34;
then A33: B c= A1 by A17, INTEGRA1:4;
for k being Nat st k in dom (v | i) holds
(v | i) . k = xvol (B /\ (divset (D1,k)))

proof

let k be Nat; :: thesis: ( k in dom (v | i) implies (v | i) . k = xvol (B /\ (divset (D1,k))) )
assume A34: k in dom (v | i) ; :: thesis: (v | i) . k = xvol (B /\ (divset (D1,k)))
then A35: ( k in Seg i & k in dom v ) by RELAT_1:57;
then A36: v . k = (v | i) . k by FUNCT_1:49;
A37: ( k in dom D & k in dom D1 ) by A34, A35, A13, A4, FINSEQ_3:29;
A38: ( divset (D,k) = [.(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).] & divset (D1,k) = [.(lower_bound (divset (D1,k))),(upper_bound (divset (D1,k))).] ) by INTEGRA1:4;
divset (D,k) = divset (D1,k)

proof

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

suppose k = 1 ; :: thesis: divset (D,k) = divset (D1,k)

then A39: ( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = D . k & lower_bound (divset (D1,k)) = lower_bound A1 & upper_bound (divset (D1,k)) = D1 . k ) by A37, INTEGRA1:def 4;
lower_bound A = lower_bound A1 by A17, A27, INTEGRA1:5;
hence divset (D,k) = divset (D1,k) by A39, A35, A38, FUNCT_1:49; :: thesis: verum

end;

suppose A40: k <> 1 ; :: thesis: divset (D,k) = divset (D1,k)

then A41: ( lower_bound (divset (D,k)) = D . (k - 1) & upper_bound (divset (D,k)) = D . k & lower_bound (divset (D1,k)) = D1 . (k - 1) & upper_bound (divset (D1,k)) = D1 . k ) by A37, INTEGRA1:def 4;
A42: 1 <= k by A35, FINSEQ_1:1;
then k - 1 in NAT by INT_1:5;
then reconsider k1 = k - 1 as Nat ;
1 < k by A40, A42, XXREAL_0:1;
then D . k1 = D1 . k1 by A35, FINSEQ_3:12, FUNCT_1:49;
hence divset (D,k) = divset (D1,k) by A41, A35, A38, FUNCT_1:49; :: thesis: verum

end;

end;

end;

hence (v | i) . k = xvol (B /\ (divset (D1,k))) by A4, A35, A36; :: thesis: verum

end;

then A43: Sum (v | i) = vol B by A3, A33, A13;
A44: [.(D . i),(upper_bound B).] c= {(D . i)} by A32, XXREAL_1:85;
lower_bound B <= upper_bound B by SEQ_4:11;
then ( lower_bound B <= D . i & upper_bound B <= D . (i + 1) ) by A32, A31, XXREAL_0:2;
then A45: B /\ (divset (D,(i + 1))) c= {(D . i)} by A44, A30, XXREAL_1:143;
reconsider BD = B /\ (divset (D,(i + 1))) as real-bounded Subset of REAL by XBOOLE_1:17, XXREAL_2:45;
A46: xvol (B /\ (divset (D,(i + 1)))) <= xvol {(D . i)}

proof

per cases ( B /\ (divset (D,(i + 1))) = {} or B /\ (divset (D,(i + 1))) <> {} ) ;

suppose B /\ (divset (D,(i + 1))) = {} ; :: thesis: xvol (B /\ (divset (D,(i + 1)))) <= xvol {(D . i)}

then xvol (B /\ (divset (D,(i + 1)))) = 0 by Def2;
hence xvol (B /\ (divset (D,(i + 1)))) <= xvol {(D . i)} by Th5; :: thesis: verum

end;

suppose B /\ (divset (D,(i + 1))) <> {} ; :: thesis: xvol (B /\ (divset (D,(i + 1)))) <= xvol {(D . i)}

then reconsider BD = B /\ (divset (D,(i + 1))) as non empty real-bounded Subset of REAL by XBOOLE_1:17, XXREAL_2:45;
reconsider Di = {(D . i)} as non empty real-bounded Subset of REAL ;
A47: ( xvol BD = vol BD & xvol {(D . i)} = vol {(D . i)} ) by Def2;
( lower_bound Di <= lower_bound BD & upper_bound BD <= upper_bound Di ) by A45, SEQ_4:47, SEQ_4:48;
hence xvol (B /\ (divset (D,(i + 1)))) <= xvol {(D . i)} by A47, XREAL_1:13; :: thesis: verum

end;

end;

end;

A48: vol {(D . i)} = (upper_bound {(D . i)}) - (upper_bound {(D . i)}) by SEQ_4:10;
0 <= xvol BD by Th5;
then v . (i + 1) = 0 by A6, A46, A48, Def2;
then Sum v = (vol B) + 0 by A43, A8, RVSUM_1:74;
hence Sum v = vol B ; :: thesis: verum

end;

suppose A49: D . i < upper_bound B ; :: thesis: Sum v = vol B

per cases ( lower_bound B <= D . i or D . i < lower_bound B ) ;

suppose A50: lower_bound B <= D . i ; :: thesis: Sum v = vol B

then reconsider B1 = [.(lower_bound B),(D . i).], B2 = [.(D . i),(upper_bound B).] as non empty closed_interval Subset of REAL by XXREAL_1:30, A49, MEASURE5:def 3;
B1 \/ B2 = [.(lower_bound B),(upper_bound B).] by A50, A49, XXREAL_1:165;
then A51: B1 \/ B2 = B by INTEGRA1:4;
( B1 = [.(lower_bound B1),(upper_bound B1).] & B2 = [.(lower_bound B2),(upper_bound B2).] ) by INTEGRA1:4;
then A52: ( lower_bound B = lower_bound B1 & D . i = upper_bound B1 & D . i = lower_bound B2 & upper_bound B = upper_bound B2 ) by INTEGRA1:5;
for k being Nat st k in dom (v | i) holds
(v | i) . k = xvol (B1 /\ (divset (D1,k)))

proof

let k be Nat; :: thesis: ( k in dom (v | i) implies (v | i) . k = xvol (B1 /\ (divset (D1,k))) )
assume A53: k in dom (v | i) ; :: thesis: (v | i) . k = xvol (B1 /\ (divset (D1,k)))
then A54: ( k in Seg i & k in dom v ) by RELAT_1:57;
then A55: v . k = xvol (B /\ (divset (D,k))) by A4;
A56: v . k = (v | i) . k by A54, FUNCT_1:49;
A57: ( k in dom D & k in dom D1 ) by A53, A54, A4, A13, FINSEQ_3:29;
A58: ( divset (D,k) = [.(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).] & divset (D1,k) = [.(lower_bound (divset (D1,k))),(upper_bound (divset (D1,k))).] ) by INTEGRA1:4;
A59: divset (D,k) = divset (D1,k)

proof

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

suppose k = 1 ; :: thesis: divset (D,k) = divset (D1,k)

then A60: ( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = D . k & lower_bound (divset (D1,k)) = lower_bound A1 & upper_bound (divset (D1,k)) = D1 . k ) by A57, INTEGRA1:def 4;
lower_bound A = lower_bound A1 by A27, A17, INTEGRA1:5;
hence divset (D,k) = divset (D1,k) by A60, A54, A58, FUNCT_1:49; :: thesis: verum

end;

suppose A61: k <> 1 ; :: thesis: divset (D,k) = divset (D1,k)

then A62: ( lower_bound (divset (D,k)) = D . (k - 1) & upper_bound (divset (D,k)) = D . k & lower_bound (divset (D1,k)) = D1 . (k - 1) & upper_bound (divset (D1,k)) = D1 . k ) by A57, INTEGRA1:def 4;
A63: 1 <= k by A54, FINSEQ_1:1;
then k - 1 in NAT by INT_1:5;
then reconsider k1 = k - 1 as Nat ;
1 < k by A61, A63, XXREAL_0:1;
then D . k1 = D1 . k1 by A54, FINSEQ_3:12, FUNCT_1:49;
hence divset (D,k) = divset (D1,k) by A62, A54, A58, FUNCT_1:49; :: thesis: verum

end;

end;

end;

then A64: B1 /\ (divset (D1,k)) c= B /\ (divset (D,k)) by A51, XBOOLE_1:7, XBOOLE_1:26;
for x being object st x in B /\ (divset (D,k)) holds
x in B1 /\ (divset (D1,k))

proof

let x be object ; :: thesis: ( x in B /\ (divset (D,k)) implies x in B1 /\ (divset (D1,k)) )
assume A65: x in B /\ (divset (D,k)) ; :: thesis: x in B1 /\ (divset (D1,k))
then reconsider r = x as Real ;
A66: ( x in B & x in divset (D,k) ) by A65, XBOOLE_0:def 4;
then A67: ex r0 being Real st
( r = r0 & lower_bound B <= r0 & r0 <= upper_bound B ) by A30;
A68: ex r1 being Real st
( r = r1 & lower_bound (divset (D,k)) <= r1 & r1 <= upper_bound (divset (D,k)) ) by A58, A66;
A69: k <= i by A54, FINSEQ_1:1;

A70: now :: thesis: ( k <> i implies D . k <= D . i )

assume k <> i ; :: thesis: D . k <= D . i
then k < i by A69, XXREAL_0:1;
hence D . k <= D . i by A16, A57, VALUED_0:def 13; :: thesis: verum

end;

( k = 1 or k <> 1 ) ;
then upper_bound (divset (D,k)) <= D . i by A70, A57, INTEGRA1:def 4;
then r <= D . i by A68, XXREAL_0:2;
then r in B1 by A67;
hence x in B1 /\ (divset (D1,k)) by XBOOLE_0:def 4, A59, A66; :: thesis: verum

end;

then B /\ (divset (D,k)) c= B1 /\ (divset (D1,k)) ;
hence (v | i) . k = xvol (B1 /\ (divset (D1,k))) by A55, A56, A64, XBOOLE_0:def 10; :: thesis: verum

end;

then A71: Sum (v | i) = vol B1 by A3, A17, A9, XXREAL_1:34, A13;
B /\ (divset (D,(i + 1))) = (B1 /\ (divset (D,(i + 1)))) \/ (B2 /\ (divset (D,(i + 1)))) by A51, XBOOLE_1:23;
then B /\ (divset (D,(i + 1))) = [.(D . i),(D . i).] \/ (B2 /\ [.(D . i),(D . (i + 1)).]) by A30, A50, A31, XXREAL_1:143;
then A72: B /\ (divset (D,(i + 1))) = ([.(D . i),(D . i).] \/ [.(D . i),(upper_bound B).]) /\ ([.(D . i),(D . i).] \/ [.(D . i),(D . (i + 1)).]) by XBOOLE_1:24;
D . i <= upper_bound B by A52, SEQ_4:11;
then A73: [.(D . i),(D . i).] \/ [.(D . i),(upper_bound B).] = B2 by XXREAL_1:165;
[.(D . i),(D . i).] \/ [.(D . i),(D . (i + 1)).] = [.(D . i),(D . (i + 1)).] by A31, XXREAL_1:165;
then A74: [.(D . i),(D . i).] \/ [.(D . i),(D . (i + 1)).] = divset (D,(i + 1)) by A29, INTEGRA1:4;
A75: upper_bound B <= D . (i + 1) by A4, A9, INTEGRA1:def 2;
for x being object st x in B2 holds
x in divset (D,(i + 1))

proof

let x be object ; :: thesis: ( x in B2 implies x in divset (D,(i + 1)) )
assume A76: x in B2 ; :: thesis: x in divset (D,(i + 1))
then reconsider r = x as Real ;
A77: ex r0 being Real st
( r = r0 & D . i <= r0 & r0 <= upper_bound B ) by A76;
r <= D . (i + 1) by A75, XXREAL_0:2, A77;
hence x in divset (D,(i + 1)) by A30, A77; :: thesis: verum

end;

then A78: B2 c= divset (D,(i + 1)) ;
v . (i + 1) = xvol (B /\ (divset (D,(i + 1)))) by A4, A5, FINSEQ_1:4;
then v . (i + 1) = xvol B2 by A78, A74, A72, A73, XBOOLE_1:28;
then v . (i + 1) = vol B2 by Def2;
then Sum v = (vol B1) + (vol B2) by A8, RVSUM_1:74, A71;
hence Sum v = vol B by A52; :: thesis: verum

end;

suppose A79: D . i < lower_bound B ; :: thesis: Sum v = vol B

then A80: [.(lower_bound B),(D . i).] = {} by XXREAL_1:29;
reconsider B1 = [.(lower_bound B),(D . i).] as Subset of REAL ;
reconsider B2 = B as non empty closed_interval Subset of REAL ;

now :: thesis: for k0 being object st k0 in dom (v | i) holds
(v | i) . k0 = 0

let k0 be object ; :: thesis: ( k0 in dom (v | i) implies (v | i) . k0 = 0 )
assume A81: k0 in dom (v | i) ; :: thesis: (v | i) . k0 = 0
then A82: ( k0 in Seg i & k0 in dom v ) by RELAT_1:57;
reconsider k = k0 as Nat by A81;
A83: ( k in dom D & k in dom D1 ) by A81, A82, A4, A13, FINSEQ_3:29;
A84: ( divset (D,k) = [.(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).] & divset (D1,k) = [.(lower_bound (divset (D1,k))),(upper_bound (divset (D1,k))).] ) by INTEGRA1:4;
A85: divset (D,k) = divset (D1,k)

proof

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

suppose k = 1 ; :: thesis: divset (D,k) = divset (D1,k)

then A86: ( lower_bound (divset (D,k)) = lower_bound A & upper_bound (divset (D,k)) = D . k & lower_bound (divset (D1,k)) = lower_bound A1 & upper_bound (divset (D1,k)) = D1 . k ) by A83, INTEGRA1:def 4;
lower_bound A = lower_bound A1 by A27, A17, INTEGRA1:5;
hence divset (D,k) = divset (D1,k) by A84, A86, A82, FUNCT_1:49; :: thesis: verum

end;

suppose A87: k <> 1 ; :: thesis: divset (D,k) = divset (D1,k)

then A88: ( lower_bound (divset (D,k)) = D . (k - 1) & upper_bound (divset (D,k)) = D . k & lower_bound (divset (D1,k)) = D1 . (k - 1) & upper_bound (divset (D1,k)) = D1 . k ) by A83, INTEGRA1:def 4;
A89: 1 <= k by A82, FINSEQ_1:1;
then k - 1 in NAT by INT_1:5;
then reconsider k1 = k - 1 as Nat ;
1 < k by A87, A89, XXREAL_0:1;
then D . k1 = D1 . k1 by A82, FINSEQ_3:12, FUNCT_1:49;
hence divset (D,k) = divset (D1,k) by A88, A82, A84, FUNCT_1:49; :: thesis: verum

end;

end;

end;

for x being object st x in B /\ (divset (D,k)) holds
x in B1 /\ (divset (D1,k))

proof

let x be object ; :: thesis: ( x in B /\ (divset (D,k)) implies x in B1 /\ (divset (D1,k)) )
assume A90: x in B /\ (divset (D,k)) ; :: thesis: x in B1 /\ (divset (D1,k))
then reconsider r = x as Real ;
A91: ( x in B & x in divset (D,k) ) by A90, XBOOLE_0:def 4;
then A92: ( ex r0 being Real st
( r = r0 & lower_bound B <= r0 & r0 <= upper_bound B ) & ex r1 being Real st
( r = r1 & lower_bound (divset (D,k)) <= r1 & r1 <= upper_bound (divset (D,k)) ) ) by A30, A84;
k in Seg i by A81, RELAT_1:57;
then A93: k <= i by FINSEQ_1:1;

A94: now :: thesis: ( k <> i implies D . k <= D . i )

assume k <> i ; :: thesis: D . k <= D . i
then k < i by A93, XXREAL_0:1;
hence D . k <= D . i by A16, A83, VALUED_0:def 13; :: thesis: verum

end;

( k = 1 or k <> 1 ) ;
then upper_bound (divset (D,k)) <= D . i by A94, A83, INTEGRA1:def 4;
then r <= D . i by A92, XXREAL_0:2;
then r in B1 by A92;
hence x in B1 /\ (divset (D1,k)) by XBOOLE_0:def 4, A85, A91; :: thesis: verum

end;

then A95: B /\ (divset (D,k)) c= B1 /\ (divset (D1,k)) ;
v . k = xvol (B /\ (divset (D,k))) by A82, A4;
then v . k0 = 0 by Def2, A80, A95;
hence (v | i) . k0 = 0 by A82, FUNCT_1:49; :: thesis: verum

end;

then v | i = (dom (v | i)) --> 0 by FUNCOP_1:11;
then v | i = i |-> 0 by A14, FINSEQ_2:def 2;
then A96: Sum (v | i) = 0 by RVSUM_1:81;
A97: upper_bound B <= D . (i + 1) by A4, A9, INTEGRA1:def 2;
for x being object st x in B2 holds
x in divset (D,(i + 1))

proof

let x be object ; :: thesis: ( x in B2 implies x in divset (D,(i + 1)) )
assume A98: x in B2 ; :: thesis: x in divset (D,(i + 1))
then reconsider r = x as Real ;
B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:4;
then ex r0 being Real st
( r = r0 & lower_bound B <= r0 & r0 <= upper_bound B ) by A98;
then ( D . i <= r & r <= D . (i + 1) ) by A97, XXREAL_0:2, A79;
hence x in divset (D,(i + 1)) by A30; :: thesis: verum

end;

then A99: B2 c= divset (D,(i + 1)) ;
v . (i + 1) = xvol (B /\ (divset (D,(i + 1)))) by A4, A5, FINSEQ_1:4;
then v . (i + 1) = xvol B by A99, XBOOLE_1:28;
then v . (i + 1) = vol B by Def2;
then Sum v = 0 + (vol B) by A8, RVSUM_1:74, A96;
hence Sum v = vol B ; :: thesis: verum

end;

end;

end;

end;

end;

suppose A100: i = 0 ; :: thesis: Sum v = vol B

then A101: D . 1 = upper_bound A by A4, INTEGRA1:def 2;
dom D = Seg 1 by A100, A4, FINSEQ_1:def 3;
then 1 in dom D ;
then ( lower_bound (divset (D,1)) = lower_bound A & upper_bound (divset (D,1)) = D . 1 ) by INTEGRA1:def 4;
then divset (D,1) = [.(lower_bound A),(upper_bound A).] by A101, INTEGRA1:4;
then A102: divset (D,1) = A by INTEGRA1:4;
v . 1 = xvol (B /\ (divset (D,1))) by A100, A4, A5, FINSEQ_1:4;
then v . 1 = xvol B by A102, A4, XBOOLE_1:28;
then A103: v . 1 = vol B by Def2;
Sum v = (Sum (v | i)) + (v . 1) by A100, A8, RVSUM_1:74;
then Sum v = 0 + (vol B) by A100, RVSUM_1:72, A103;
hence Sum v = vol B ; :: thesis: verum

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
hence for A being non empty closed_interval Subset of REAL
for D being Division of A
for B being non empty closed_interval Subset of REAL
for v being FinSequence of REAL st B c= A & len D = len v & ( for i being Nat st i in dom v holds
v . i = xvol (B /\ (divset (D,i))) ) holds
Sum v = vol B ; :: thesis: verum