let rho be real-valued Function; :: thesis:
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 A c= dom rho & $1 = len D & B c= A & len D = len v & ( for k being Nat st k in dom v holds
v . k = vol ((B /\ (divset (D,k))),rho) ) holds
Sum v = vol (B,rho);
A1: S₁[ 0 ] ;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume A3: S₁[i] ; :: thesis:
let A be non empty closed_interval Subset of REAL; :: thesis:
let D be Division of A; :: thesis:
let B be non empty closed_interval Subset of REAL; :: thesis:
let v be FinSequence of REAL ; :: thesis:
set D1 = D | i;
set v1 = v | i;
assume A4: ( A c= dom rho & i + 1 = len D & B c= A & len D = len v & ( for k being Nat st k in dom v holds
v . k = vol ((B /\ (divset (D,k))),rho) ) ) ; :: thesis:
A5: ( dom D = Seg (i + 1) & dom D = dom v ) by A4, FINSEQ_1:def 3, FINSEQ_3:29;
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;
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 ;

suppose A15: i <> 0 ; :: thesis:

then A16: i in dom D by A12, FINSEQ_1:3, TARSKI:def 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;
A1 c= A by A17, XBOOLE_1:7;
then B17: A1 c= dom rho by A4, XBOOLE_1:1;
B23: for y being object st y in rng (D | i) holds
y in A1

proof

let y be object ; :: thesis:
assume A18: y in rng (D | i) ; :: thesis:
then y in A by A11, TARSKI:def 3, INTEGRA1:def 2;
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:

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

end;

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

end;

A24: (D | i) . i = D . i by A15, FINSEQ_1:3, FUNCT_1:49;
for e1, e2 being ExtReal st e1 in dom (D | i) & e2 in dom (D | i) & e1 < e2 holds
(D | i) . e1 < (D | i) . e2

proof

let e1, e2 be ExtReal; :: thesis:
assume A25: ( e1 in dom (D | i) & e2 in dom (D | i) & e1 < e2 ) ; :: thesis:
then A26: ( e1 in Seg i & e2 in Seg i ) by A13, FINSEQ_1:def 3;
then ( (D | i) . e1 = D . e1 & (D | i) . e2 = D . e2 ) by FUNCT_1:49;
hence (D | i) . e1 < (D | i) . e2 by A25, VALUED_0:def 13, A26, A12; :: thesis:

end;

then reconsider D1 = D | i as non empty increasing FinSequence of REAL by A15, VALUED_0:def 13;
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 INTEGRA1:def 2, TARSKI:def 3, B23;
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 ;

suppose A32: upper_bound B < D . i ; :: thesis:

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 = vol ((B /\ (divset (D1,k))),rho)

proof

let k be Nat; :: thesis:
assume A34: k in dom (v | i) ; :: thesis:
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, A4, FINSEQ_3:29, A13;
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 ;

suppose k = 1 ; :: thesis:

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:

end;

suppose A40: k <> 1 ; :: thesis:

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:

end;

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

end;

then A43: Sum (v | i) = vol (B,rho) by A3, A33, A13, B17;
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 B /\ (divset (D,(i + 1))) = [.(D . i),(upper_bound B).] by A30, XXREAL_1:143
.= {} by A32, XXREAL_1:29 ;
then vol ((B /\ (divset (D,(i + 1)))),rho) = 0 by Defvol;
then v . (i + 1) = 0 by A5, A4, FINSEQ_1:4;
then Sum v = (vol (B,rho)) + 0 by A43, A8, RVSUM_1:74;
hence Sum v = vol (B,rho) ; :: thesis:

end;

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

per cases ;

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

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 = vol ((B1 /\ (divset (D1,k))),rho)

proof

let k be Nat; :: thesis:
assume A53: k in dom (v | i) ; :: thesis:
then A54: ( k in Seg i & k in dom v ) by RELAT_1:57;
then A55: v . k = vol ((B /\ (divset (D,k))),rho) 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 ;

suppose k = 1 ; :: thesis:

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:

end;

suppose A61: k <> 1 ; :: thesis:

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:

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:
assume A65: x in B /\ (divset (D,k)) ; :: thesis:
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:

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

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:

end;

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

end;

then A71: Sum (v | i) = vol (B1,rho) by A3, A17, A9, XXREAL_1:34, A13, B17;
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;
C78: for x being object st x in B2 holds
x in divset (D,(i + 1))

proof

let x be object ; :: thesis:
assume A76: x in B2 ; :: thesis:
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:

end;

v . (i + 1) = vol ((B /\ (divset (D,(i + 1)))),rho) by A4, A5, FINSEQ_1:4;
then D78: v . (i + 1) = vol (B2,rho) by TARSKI:def 3, C78, A74, A72, A73, XBOOLE_1:28;
B79: vol (B1,rho) = (rho . (D . i)) - (rho . (lower_bound B)) by A52, Defvol;
vol (B2,rho) = (rho . (upper_bound B)) - (rho . (D . i)) by A52, Defvol;
then (vol (B1,rho)) + (vol (B2,rho)) = (rho . (upper_bound B)) - (rho . (lower_bound B)) by B79
.= vol (B,rho) by Defvol ;
hence Sum v = vol (B,rho) by D78, A8, RVSUM_1:74, A71; :: thesis:

end;

suppose A79: D . i < lower_bound B ; :: thesis:

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:

let k0 be object ; :: thesis:
assume A81: k0 in dom (v | i) ; :: thesis:
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 ;

suppose k = 1 ; :: thesis:

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:

end;

suppose A87: k <> 1 ; :: thesis:

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:

end;

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

proof

let x be object ; :: thesis:
assume A90: x in B /\ (divset (D,k)) ; :: thesis:
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:

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

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:

end;

C95: B /\ (divset (D,k)) = {} by TARSKI:def 3, B95, XBOOLE_1:3, A80;
v . k = vol ((B /\ (divset (D,k))),rho) by A82, A4;
then v . k0 = 0 by C95, Defvol;
hence (v | i) . k0 = 0 by A82, FUNCT_1:49; :: thesis:

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;
B99: for x being object st x in B2 holds
x in divset (D,(i + 1))

proof

let x be object ; :: thesis:
assume A98: x in B2 ; :: thesis:
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:

end;

v . (i + 1) = vol ((B /\ (divset (D,(i + 1)))),rho) by A4, A5, FINSEQ_1:4;
then v . (i + 1) = vol (B,rho) by TARSKI:def 3, B99, XBOOLE_1:28;
then Sum v = 0 + (vol (B,rho)) by A8, RVSUM_1:74, A96;
hence Sum v = vol (B,rho) ; :: thesis:

end;

suppose A100: i = 0 ; :: thesis:

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 = vol ((B /\ (divset (D,1))),rho) by A100, A4, A5, FINSEQ_1:4;
then A103: v . 1 = vol (B,rho) by A102, A4, XBOOLE_1:28;
Sum v = (Sum (v | i)) + (v . 1) by A100, A8, RVSUM_1:74;
then Sum v = 0 + (vol (B,rho)) by A100, RVSUM_1:72, A103;
hence Sum v = vol (B,rho) ; :: thesis:

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 A c= dom rho & B c= A & len D = len v & ( for i being Nat st i in dom v holds
v . i = vol ((B /\ (divset (D,i))),rho) ) holds
Sum v = vol (B,rho) ; :: thesis: