let A be non empty closed_interval Subset of REAL; :: thesis:
let T be Division of A; :: thesis:
let rho be real-valued Function; :: thesis:
defpred S₁[ Nat] means for B being non empty closed_interval Subset of REAL
for S0 being non empty increasing FinSequence of REAL
for ST being FinSequence of REAL st B c= A & lower_bound B = lower_bound A & len S0 = $1 & ex S being Division of B st
( S = S0 & len ST = len S & ( for j being Nat st j in dom S holds
ex p being FinSequence of REAL st
( ST . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S,j))),rho)).| ) ) ) ) holds
ex H being Division of B ex F being var_volume of rho,H st Sum ST = Sum F;
A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A3: S₁[k] ; :: thesis:
let B be non empty closed_interval Subset of REAL; :: thesis:
let S0 be non empty increasing FinSequence of REAL ; :: thesis:
let ST be FinSequence of REAL ; :: thesis:
assume A4: ( B c= A & lower_bound B = lower_bound A & len S0 = k + 1 & ex S being Division of B st
( S = S0 & len ST = len S & ( for j being Nat st j in dom S holds
ex p being FinSequence of REAL st
( ST . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S,j))),rho)).| ) ) ) ) ) ; :: thesis:
then consider S being Division of B such that
A5: ( S = S0 & len ST = len S & ( for j being Nat st j in dom S holds
ex p being FinSequence of REAL st
( ST . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S,j))),rho)).| ) ) ) ) ;
Z: dom ST = dom S by A5, FINSEQ_3:29;

per cases ;

suppose A6: k = 0 ; :: thesis:

set IDX = { i where i is Nat : ( i in dom T & T . i < upper_bound B ) } ;
{ i where i is Nat : ( i in dom T & T . i < upper_bound B ) } c= dom T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { i where i is Nat : ( i in dom T & T . i < upper_bound B ) } ; :: thesis:
then ex i being Nat st
( x = i & i in dom T & T . i < upper_bound B ) ;
hence x in dom T ; :: thesis:

end;

then reconsider IDX = { i where i is Nat : ( i in dom T & T . i < upper_bound B ) } as finite Subset of NAT by XBOOLE_1:1;
a: 1 <= len T by NAT_1:14;
then A7: 1 in dom T by FINSEQ_3:25;
ST = <*(ST . 1)*> by A4, A6, FINSEQ_1:40;
then A8: Sum ST = ST . 1 by RVSUM_1:73;
A10: 1 in dom S by A4, A5, A6, FINSEQ_3:25;
A11: S . 1 = upper_bound B by A4, A5, A6, INTEGRA1:def 2;

per cases ;

suppose A12: IDX = {} ; :: thesis:

set F = the var_volume of rho,S;
take S ; :: thesis:
take the var_volume of rho,S ; :: thesis:
the var_volume of rho,S = <*( the var_volume of rho,S . 1)*> by A4, A5, A6, FINSEQ_1:40, INTEGR22:def 2;
then A13: Sum the var_volume of rho,S = the var_volume of rho,S . 1 by RVSUM_1:73;
not 1 in IDX by A12;
then A14: upper_bound B <= T . 1 by A7;
A15: the var_volume of rho,S . 1 = |.(vol ((divset (S,1)),rho)).| by A4, A5, A6, FINSEQ_3:25, INTEGR22:def 2;
consider p being FinSequence of REAL such that
A16: ( ST . 1 = Sum p & len p = len T & ( for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S,1))),rho)).| ) ) by A4, A5, A6, FINSEQ_3:25;
Z: dom p = dom T by A16, FINSEQ_3:29;
A18: p . 1 = |.(vol (((divset (T,1)) /\ (divset (S,1))),rho)).| by FINSEQ_3:25, a, A16;
A19: divset (S,1) c= B by A4, A5, A6, FINSEQ_3:25, INTEGRA1:8;
A20: B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:4;
A22: ( lower_bound (divset (T,1)) = lower_bound A & upper_bound (divset (T,1)) = T . 1 ) by INTEGRA1:def 4, A7;
[.(lower_bound B),(upper_bound B).] c= [.(lower_bound (divset (T,1))),(upper_bound (divset (T,1))).] by A4, A14, A22, XXREAL_1:34;
then [.(lower_bound B),(upper_bound B).] c= divset (T,1) by INTEGRA1:4;
then divset (S,1) c= divset (T,1) by A19, A20;
then A23: p . 1 = |.(vol ((divset (S,1)),rho)).| by A18, XBOOLE_1:28;
for i being Nat st i in dom p & i <> 1 holds
p . i = 0

proof

let i be Nat; :: thesis:
assume A24: ( i in dom p & i <> 1 ) ; :: thesis:
then A26: ( 1 <= i & i <= len p ) by FINSEQ_3:25;
then 1 < i by A24, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then A27: 2 - 1 <= i - 1 by XREAL_1:9;
then reconsider i1 = i - 1 as Nat by INT_1:3, ORDINAL1:def 12;
i - 1 <= (len p) - 0 by A26, XREAL_1:13;
then i1 in dom T by A16, A27, FINSEQ_3:25;
then A28: T . 1 <= T . (i - 1) by A7, A27, VALUED_0:def 15;
A29: ( lower_bound (divset (T,i)) = T . (i - 1) & upper_bound (divset (T,i)) = T . i ) by Z, A24, INTEGRA1:def 4;
dom p = dom T by FINSEQ_3:29, A16;
then A30: p . i = |.(vol (((divset (T,i)) /\ (divset (S,1))),rho)).| by A16, A24;
(divset (T,i)) /\ (divset (S,1)) c= (divset (T,i)) /\ B by A10, INTEGRA1:8, XBOOLE_1:26;
then A31: (divset (T,i)) /\ (divset (S,1)) c= [.(lower_bound B),(upper_bound B).] /\ [.(lower_bound (divset (T,i))),(upper_bound (divset (T,i))).] by A20, INTEGRA1:4;
[.(lower_bound B),(upper_bound B).] /\ [.(lower_bound (divset (T,i))),(upper_bound (divset (T,i))).] c= [.(upper_bound B),(upper_bound B).] by A14, A28, A29, Th10, XXREAL_0:2;
then (divset (T,i)) /\ (divset (S,1)) c= [.(upper_bound B),(upper_bound B).] by A31;
hence p . i = 0 by A30, COMPLEX1:44, Th11; :: thesis:

end;

hence Sum ST = Sum the var_volume of rho,S by A8, A13, A15, A16, a, FINSEQ_3:25, A23, Th8; :: thesis:

end;

suppose A32: IDX <> {} ; :: thesis:

A33: sup IDX in IDX by A32, XXREAL_2:def 6;
then reconsider n = sup IDX as Nat ;
A34: ex i being Nat st
( n = i & i in dom T & T . i < upper_bound B ) by A33;
A35: ( 1 <= n & n <= len T ) by A34, FINSEQ_3:25;
n <> len T

proof

assume n = len T ; :: thesis:
then upper_bound A < upper_bound B by A34, INTEGRA1:def 2;
hence contradiction by A4, XXREAL_2:59; :: thesis:

end;

then n < len T by A35, XXREAL_0:1;
then A37: ( 1 <= n + 1 & n + 1 <= len T ) by NAT_1:11, NAT_1:13;
then A38: n + 1 in dom T by FINSEQ_3:25;
A39: upper_bound B <= T . (n + 1)

proof

assume T . (n + 1) < upper_bound B ; :: thesis:
then n + 1 in IDX by A38;
hence contradiction by NAT_1:16, XXREAL_2:4; :: thesis:

end;

set H = (T | n) ^ <*(upper_bound B)*>;
upper_bound B is Element of REAL by XREAL_0:def 1;
then A40: <*(upper_bound B)*> is FinSequence of REAL by FINSEQ_1:74;
A41: len (T | n) = n by A35, FINSEQ_1:59;
len <*(upper_bound B)*> = 1 by FINSEQ_1:39;
then A42: len ((T | n) ^ <*(upper_bound B)*>) = n + 1 by A41, FINSEQ_1:22;
reconsider H = (T | n) ^ <*(upper_bound B)*> as non empty FinSequence of REAL by A40, FINSEQ_1:75;
for e1, e2 being ExtReal st e1 in dom H & e2 in dom H & e1 < e2 holds
H . e1 < H . e2

proof

let e1, e2 be ExtReal; :: thesis:
assume A43: ( e1 in dom H & e2 in dom H & e1 < e2 ) ; :: thesis:
then reconsider i = e1, j = e2 as Nat ;
A45: ( 1 <= i & i <= n + 1 & 1 <= j & j <= n + 1 ) by A42, A43, FINSEQ_3:25;

per cases ;

suppose A46: j = n + 1 ; :: thesis:

then A47: H . e2 = upper_bound B by A41, FINSEQ_1:42;
A48: i <= n by A43, A46, NAT_1:13;
then A49: i in dom (T | n) by A41, A45, FINSEQ_3:25;
then A50: H . e1 = (T | n) . i by FINSEQ_1:def 7
.= T . i by A49, FUNCT_1:47 ;
i <= len T by A37, A43, A46, XXREAL_0:2;
then i in dom T by A45, FINSEQ_3:25;
then T . i <= T . n by A34, A48, VALUED_0:def 15;
hence H . e1 < H . e2 by A34, A47, A50, XXREAL_0:2; :: thesis:

end;

suppose j <> n + 1 ; :: thesis:

then j < n + 1 by A45, XXREAL_0:1;
then A52: j <= n by NAT_1:13;
then A53: j in dom (T | n) by A41, A45, FINSEQ_3:25;
then A54: H . e2 = (T | n) . j by FINSEQ_1:def 7
.= T . j by A53, FUNCT_1:47 ;
A55: i <= n by A43, A52, XXREAL_0:2;
then A56: i in dom (T | n) by A41, A45, FINSEQ_3:25;
then A57: H . e1 = (T | n) . i by FINSEQ_1:def 7
.= T . i by A56, FUNCT_1:47 ;
i <= len T by A35, A55, XXREAL_0:2;
then A58: i in dom T by A45, FINSEQ_3:25;
j <= len T by A35, A52, XXREAL_0:2;
then j in dom T by A45, FINSEQ_3:25;
hence H . e1 < H . e2 by A43, A54, A57, A58, VALUED_0:def 13; :: thesis:

end;

then reconsider H = H as non empty increasing FinSequence of REAL by VALUED_0:def 13;
A59: B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:4;
A60: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
A61: H . (len H) = upper_bound B by A41, A42, FINSEQ_1:42;
A62: rng H = (rng (T | n)) \/ (rng <*(upper_bound B)*>) by FINSEQ_1:31;
A63: rng <*(upper_bound B)*> = {(upper_bound B)} by FINSEQ_1:39;
A64: rng (T | n) c= rng T by RELAT_1:70;
rng T c= A by INTEGRA1:def 2;
then A65: rng (T | n) c= A by A64;
lower_bound B <= upper_bound B by SEQ_4:11;
then upper_bound B in B by A59;
then {(upper_bound B)} c= A by A4, ZFMISC_1:31;
then A66: rng H c= A by A62, A63, A65, XBOOLE_1:8;
for z being object st z in rng H holds
z in B

proof

let z be object ; :: thesis:
assume A67: z in rng H ; :: thesis:
then reconsider x = z as Real ;
x in A by A66, A67;
then A68: ex r being Real st
( x = r & lower_bound A <= r & r <= upper_bound A ) by A60;
consider i being object such that
A69: ( i in dom H & x = H . i ) by A67, FUNCT_1:def 3;
reconsider i = i as Nat by A69;
A70: ( 1 <= i & i <= len H ) by A69, FINSEQ_3:25;
( 1 <= len H & len H <= len H ) by A70, XXREAL_0:2;
then len H in dom H by FINSEQ_3:25;
then x <= upper_bound B by A61, A69, A70, VALUED_0:def 15;
hence z in B by A4, A59, A68; :: thesis:

end;

then A71: rng H c= B ;
reconsider H = H as Division of B by A61, A71, INTEGRA1:def 2;
set F = the var_volume of rho,H;
take H ; :: thesis:
take the var_volume of rho,H ; :: thesis:
A72: len the var_volume of rho,H = len H by INTEGR22:def 2;
ST = <*(ST . 1)*> by A4, A6, FINSEQ_1:40;
then A73: Sum ST = ST . 1 by RVSUM_1:73;
consider p being FinSequence of REAL such that
A74: ( ST . 1 = Sum p & len p = len T & ( for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S,1))),rho)).| ) ) by A4, A5, A6, FINSEQ_3:25;
for i being Nat st i in dom p holds
( ( i <= len the var_volume of rho,H implies p . i = the var_volume of rho,H . i ) & ( len the var_volume of rho,H < i implies p . i = 0 ) )

proof

let i be Nat; :: thesis:
assume A75: i in dom p ; :: thesis:
dom p = dom T by A74, FINSEQ_3:29;
then A76: p . i = |.(vol (((divset (T,i)) /\ (divset (S,1))),rho)).| by A74, A75;
A77: ( 1 <= i & i <= len T ) by A74, A75, FINSEQ_3:25;
A78: ( lower_bound (divset (S,1)) = lower_bound B & upper_bound (divset (S,1)) = S . 1 ) by A10, INTEGRA1:def 4;
A79: divset (S,1) = [.(lower_bound B),(upper_bound B).] by A11, A78, INTEGRA1:4;
thus ( i <= len the var_volume of rho,H implies p . i = the var_volume of rho,H . i ) :: thesis:

proof

assume i <= len the var_volume of rho,H ; :: thesis:
then A80: ( 1 <= i & i <= len H ) by A75, FINSEQ_3:25, INTEGR22:def 2;
then A81: i in dom H by FINSEQ_3:25;
(divset (T,i)) /\ (divset (S,1)) = divset (H,i)

proof

per cases ;

suppose i <> n + 1 ; :: thesis:

then i < n + 1 by A42, A80, XXREAL_0:1;
then A82: i <= n by NAT_1:13;
then A83: i in dom (T | n) by A41, A80, FINSEQ_3:25;
then A84: H . i = (T | n) . i by FINSEQ_1:def 7
.= T . i by A83, FUNCT_1:47 ;
A85: i in dom T by A83, RELAT_1:57;
then T . i <= T . n by A34, A82, VALUED_0:def 15;
then A86: T . i <= upper_bound B by A34, XXREAL_0:2;
thus (divset (T,i)) /\ (divset (S,1)) = divset (H,i) :: thesis:

proof

per cases ;

suppose A87: i = 1 ; :: thesis:

then A88: ( lower_bound (divset (T,i)) = lower_bound A & upper_bound (divset (T,i)) = T . i ) by A85, INTEGRA1:def 4;
A89: ( lower_bound (divset (H,i)) = lower_bound B & upper_bound (divset (H,i)) = H . i ) by A81, A87, INTEGRA1:def 4;
A90: divset (T,i) = [.(lower_bound B),(T . i).] by A4, A88, INTEGRA1:4;
divset (H,i) = [.(lower_bound B),(T . i).] by A84, A89, INTEGRA1:4
.= divset (T,i) by A4, A88, INTEGRA1:4 ;
hence (divset (T,i)) /\ (divset (S,1)) = divset (H,i) by A79, A86, A90, XBOOLE_1:28, XXREAL_1:34; :: thesis:

end;

suppose A91: i <> 1 ; :: thesis:

then A92: ( lower_bound (divset (T,i)) = T . (i - 1) & upper_bound (divset (T,i)) = T . i ) by A85, INTEGRA1:def 4;
A93: ( lower_bound (divset (H,i)) = H . (i - 1) & upper_bound (divset (H,i)) = H . i ) by A81, A91, INTEGRA1:def 4;
1 < i by A77, A91, XXREAL_0:1;
then A94: 1 - 1 < i - 1 by XREAL_1:14;
then reconsider i1 = i - 1 as Nat by INT_1:3, ORDINAL1:def 12;
A95: 1 <= i1 by A94, NAT_1:14;
i1 <= (n + 1) - 1 by A42, A80, XREAL_1:13;
then A96: i - 1 in dom (T | n) by A41, A95, FINSEQ_3:25;
then H . (i - 1) = (T | n) . (i - 1) by FINSEQ_1:def 7
.= T . (i - 1) by A96, FUNCT_1:47 ;
then A98: divset (H,i) = [.(T . (i - 1)),(T . i).] by A84, A93, INTEGRA1:4;
A99: divset (T,i) = [.(T . (i - 1)),(T . i).] by A92, INTEGRA1:4;
i - 1 in dom T by A96, RELAT_1:57;
then T . (i - 1) in A by INTEGRA1:6;
then ex r being Real st
( r = T . (i - 1) & lower_bound A <= r & r <= upper_bound A ) by A60;
hence (divset (T,i)) /\ (divset (S,1)) = divset (H,i) by A4, A79, A86, A98, A99, XBOOLE_1:28, XXREAL_1:34; :: thesis:

end;

suppose A100: i = n + 1 ; :: thesis:

A101: 1 < i by A35, A100, NAT_1:16;
A102: ( lower_bound (divset (T,i)) = T . (i - 1) & upper_bound (divset (T,i)) = T . i ) by A38, A100, A101, INTEGRA1:def 4;
A103: ( lower_bound (divset (H,i)) = H . (i - 1) & upper_bound (divset (H,i)) = H . i ) by A81, A101, INTEGRA1:def 4;
reconsider i1 = i - 1 as Nat by A100;
A104: i - 1 in dom (T | n) by A35, A41, A100, FINSEQ_3:25;
then A105: H . (i - 1) = (T | n) . (i - 1) by FINSEQ_1:def 7
.= T . (i - 1) by A104, FUNCT_1:47 ;
T . (i - 1) in A by A34, A100, INTEGRA1:6;
then A106: ex r being Real st
( r = T . (i - 1) & lower_bound A <= r & r <= upper_bound A ) by A60;
thus (divset (T,i)) /\ (divset (S,1)) = [.(T . (i - 1)),(T . i).] /\ [.(lower_bound B),(upper_bound B).] by A79, A102, INTEGRA1:4
.= [.(T . (i - 1)),(upper_bound B).] by A4, A39, A100, A106, XXREAL_1:143
.= [.(H . (i - 1)),(H . i).] by A41, A100, A105, FINSEQ_1:42
.= divset (H,i) by A103, INTEGRA1:4 ; :: thesis:

end;

hence p . i = the var_volume of rho,H . i by A76, A81, INTEGR22:def 2; :: thesis:

end;

thus ( len the var_volume of rho,H < i implies p . i = 0 ) :: thesis:

proof

assume A107: len the var_volume of rho,H < i ; :: thesis:
then A108: len H < i by INTEGR22:def 2;
A109: 1 <= n + 1 by NAT_1:11;
i in dom T by A75, A74, FINSEQ_3:29;
then ( lower_bound (divset (T,i)) = T . (i - 1) & upper_bound (divset (T,i)) = T . i ) by A42, A72, A107, A109, INTEGRA1:def 4;
then A110: divset (T,i) = [.(T . (i - 1)),(T . i).] by INTEGRA1:4;
(n + 1) + 1 <= i by A42, A108, NAT_1:13;
then A111: ((n + 1) + 1) - 1 <= i - 1 by XREAL_1:9;
1 <= n + 1 by NAT_1:11;
then A112: 1 <= i - 1 by A111, XXREAL_0:2;
reconsider i1 = i - 1 as Nat by A111, INT_1:3, ORDINAL1:def 12;
i - 1 <= i - 0 by XREAL_1:13;
then i - 1 <= len T by A77, XXREAL_0:2;
then i1 in dom T by A112, FINSEQ_3:25;
then T . (n + 1) <= T . i1 by A38, A111, VALUED_0:def 15;
then (divset (T,i)) /\ (divset (S,1)) c= [.(upper_bound B),(upper_bound B).] by A39, A79, A110, Th10, XXREAL_0:2;
hence p . i = 0 by A76, COMPLEX1:44, Th11; :: thesis:

end;

hence Sum ST = Sum the var_volume of rho,H by A37, A42, A72, A73, A74, Th9; :: thesis:

end;

suppose A114: k <> 0 ; :: thesis:

set S01 = S0 | k;
A115: B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:4;
A116: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
A117: k = len (S0 | k) by A4, FINSEQ_1:59, NAT_1:11;
dom S0 = Seg (k + 1) by A4, FINSEQ_1:def 3;
then A118: Seg k c= dom S0 by FINSEQ_1:5, NAT_1:11;
for e1, e2 being ExtReal st e1 in dom (S0 | k) & e2 in dom (S0 | k) & e1 < e2 holds
(S0 | k) . e1 < (S0 | k) . e2

proof

let e1, e2 be ExtReal; :: thesis:
assume A119: ( e1 in dom (S0 | k) & e2 in dom (S0 | k) & e1 < e2 ) ; :: thesis:
then A120: ( e1 in Seg k & e2 in Seg k ) by A117, FINSEQ_1:def 3;
then ( (S0 | k) . e1 = S0 . e1 & (S0 | k) . e2 = S0 . e2 ) by FUNCT_1:49;
hence (S0 | k) . e1 < (S0 | k) . e2 by A118, A119, A120, VALUED_0:def 13; :: thesis:

end;

then reconsider S01 = S0 | k as non empty increasing FinSequence of REAL by A114, VALUED_0:def 13;
A121: k in dom S0 by A114, A118, FINSEQ_1:3;
then consider B1, B2 being non empty closed_interval Subset of REAL such that
A122: ( B1 = [.(lower_bound B),(S0 . k).] & B2 = [.(S0 . k),(upper_bound B).] & B = B1 \/ B2 ) by A5, INTEGRA1:32;
A123: B1 c= B by A122, XBOOLE_1:7;
then A124: B1 c= A by A4;
A125: B1 = [.(lower_bound B1),(upper_bound B1).] by INTEGRA1:4;
then A126: upper_bound B1 = S . k by A5, A122, INTEGRA1:5;
A127: lower_bound B1 = lower_bound A by A4, A122, A125, INTEGRA1:5;
A128: rng S0 c= B by A5, INTEGRA1:def 2;
A129: rng S01 c= rng S0 by RELAT_1:70;
for y being object st y in rng S01 holds
y in B1

proof

let y be object ; :: thesis:
assume A130: y in rng S01 ; :: thesis:
then y in B by A128, A129;
then y in [.(lower_bound B),(upper_bound B).] by INTEGRA1:4;
then consider y1 being Real such that
A131: ( y = y1 & lower_bound B <= y1 & y1 <= upper_bound B ) ;
consider x being object such that
A132: ( x in dom S01 & y1 = S01 . x ) by A130, A131, FUNCT_1:def 3;
reconsider x = x as Nat by A132;
A133: x in Seg k by A117, A132, FINSEQ_1:def 3;
then A134: x <= k by FINSEQ_1:1;

now :: thesis:

assume x <> k ; :: thesis:
then x < k by A134, XXREAL_0:1;
hence S0 . x <= S0 . k by A118, A121, A133, VALUED_0:def 13; :: thesis:

end;

then y1 <= S0 . k by A132, A133, FUNCT_1:49;
hence y in B1 by A122, A131; :: thesis:

end;

then A135: rng S01 c= B1 ;
A136: S01 . k = S0 . k by A114, FINSEQ_1:3, FUNCT_1:49;
A137: B1 = [.(lower_bound B1),(upper_bound B1).] by INTEGRA1:4;
then S01 . (len S01) = upper_bound B1 by A117, A122, A136, INTEGRA1:5;
then reconsider S1 = S01 as Division of B1 by A135, INTEGRA1:def 2;
reconsider ST1 = ST | k as FinSequence of REAL ;
A138: len S1 = k by A4, FINSEQ_1:59, NAT_1:11;
A139: len ST1 = len S1 by A4, A138, FINSEQ_1:59, NAT_1:11;
for j being Nat st j in dom S1 holds
ex p being FinSequence of REAL st
( ST1 . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S1,j))),rho)).| ) )

proof

let j be Nat; :: thesis:
assume A140: j in dom S1 ; :: thesis:
then A141: ( j in Seg k & j in dom S0 ) by RELAT_1:57;
then consider p being FinSequence of REAL such that
A142: ( ST . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S,j))),rho)).| ) ) by A5;
A143: for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S1,j))),rho)).|

proof

let i be Nat; :: thesis:
assume A144: i in dom T ; :: thesis:
A145: ( divset (S,j) = [.(lower_bound (divset (S,j))),(upper_bound (divset (S,j))).] & divset (S1,j) = [.(lower_bound (divset (S1,j))),(upper_bound (divset (S1,j))).] ) by INTEGRA1:4;
divset (S,j) = divset (S1,j)

proof

per cases ;

suppose j = 1 ; :: thesis:

then A146: ( lower_bound (divset (S,j)) = lower_bound B & upper_bound (divset (S,j)) = S . j & lower_bound (divset (S1,j)) = lower_bound B1 & upper_bound (divset (S1,j)) = S1 . j ) by A5, A140, A141, INTEGRA1:def 4;
lower_bound B = lower_bound B1 by A122, A137, INTEGRA1:5;
hence divset (S,j) = divset (S1,j) by A5, A140, A145, A146, FUNCT_1:47; :: thesis:

end;

suppose A147: j <> 1 ; :: thesis:

then A148: ( lower_bound (divset (S,j)) = S . (j - 1) & upper_bound (divset (S,j)) = S . j & lower_bound (divset (S1,j)) = S1 . (j - 1) & upper_bound (divset (S1,j)) = S1 . j ) by A5, A140, A141, INTEGRA1:def 4;
A149: 1 <= j by A141, FINSEQ_1:1;
then j - 1 in NAT by INT_1:5;
then reconsider j1 = j - 1 as Nat ;
1 < j by A147, A149, XXREAL_0:1;
then S . j1 = S1 . j1 by A5, A141, FINSEQ_3:12, FUNCT_1:49;
hence divset (S,j) = divset (S1,j) by A5, A140, A145, A148, FUNCT_1:47; :: thesis:

end;

hence p . i = |.(vol (((divset (T,i)) /\ (divset (S1,j))),rho)).| by A142, A144; :: thesis:

end;

take p ; :: thesis:
thus ( ST1 . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S1,j))),rho)).| ) ) by A141, A142, A143, FUNCT_1:49; :: thesis:

end;

then consider H1 being Division of B1, F1 being var_volume of rho,H1 such that
A150: Sum ST1 = Sum F1 by A3, A124, A127, A138, A139;
A151: ( 1 <= k + 1 & k + 1 <= len ST ) by A4, NAT_1:11;
ST = (ST | k) ^ <*(ST /. (k + 1))*> by A4, FINSEQ_5:21;
then A152: ST = ST1 ^ <*(ST . (k + 1))*> by A151, FINSEQ_4:15;
dom ST = Seg (k + 1) by A4, FINSEQ_1:def 3;
then consider p being FinSequence of REAL such that
A153: ( ST . (k + 1) = Sum p & len p = len T & ( for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S,(k + 1)))),rho)).| ) ) by Z, A5, FINSEQ_1:4;
set JDX = { i where i is Nat : ( i in dom T & upper_bound B <= T . i ) } ;
{ i where i is Nat : ( i in dom T & upper_bound B <= T . i ) } c= dom T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { i where i is Nat : ( i in dom T & upper_bound B <= T . i ) } ; :: thesis:
then ex i being Nat st
( x = i & i in dom T & upper_bound B <= T . i ) ;
hence x in dom T ; :: thesis:

end;

then reconsider JDX = { i where i is Nat : ( i in dom T & upper_bound B <= T . i ) } as finite Subset of NAT by XBOOLE_1:1;
H: dom p = dom T by FINSEQ_3:29, A153;
A154: upper_bound B <= upper_bound A by A4, XXREAL_2:59;
A155: T . (len T) = upper_bound A by INTEGRA1:def 2;
A156: 1 <= len T by NAT_1:14;
then A157: 1 in dom T by FINSEQ_3:25;
reconsider m = min* JDX as Nat ;
A159: S . (len S) = upper_bound B by INTEGRA1:def 2;
len T in dom T by A156, FINSEQ_3:25;
then len T in JDX by A154, A155;
then m in JDX by NAT_1:def 1;
then consider i being Nat such that
A160: ( m = i & i in dom T & upper_bound B <= T . i ) ;
A161: 1 <= k by A114, NAT_1:14;
k <= k + 1 by NAT_1:11;
then k in Seg (k + 1) by A161;
then A162: k in dom S by A4, A5, FINSEQ_1:def 3;
then S . k in B by INTEGRA1:6;
then A163: ex r being Real st
( r = S . k & lower_bound B <= r & r <= upper_bound B ) by A115;
A164: for i being Nat st m <= i & i in dom T holds
upper_bound B <= T . i

proof

let i be Nat; :: thesis:
assume ( m <= i & i in dom T ) ; :: thesis:
then T . m <= T . i by A160, VALUED_0:def 15;
hence upper_bound B <= T . i by A160, XXREAL_0:2; :: thesis:

end;

k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A167: k + 1 in dom S by A4, A5, FINSEQ_1:def 3;
S . k < S . (k + 1) by A162, A167, NAT_1:16, VALUED_0:def 13;
then A168: S . k < upper_bound B by A4, A5, INTEGRA1:def 2;
A169: divset (S,(k + 1)) = [.(lower_bound (divset (S,(k + 1)))),(upper_bound (divset (S,(k + 1)))).] by INTEGRA1:4;
k + 1 <> 1 by A114;
then A170: ( lower_bound (divset (S,(k + 1))) = S . ((k + 1) - 1) & upper_bound (divset (S,(k + 1))) = S . (k + 1) ) by A167, INTEGRA1:def 4;
A171: S . (k + 1) = upper_bound B by A4, A5, INTEGRA1:def 2;

per cases ;

suppose A172: m = 1 ; :: thesis:

set H = H1 ^ <*(upper_bound B)*>;
A173: upper_bound B <= T . 1 by A156, A164, A172, FINSEQ_3:25;
upper_bound B is Element of REAL by XREAL_0:def 1;
then A174: <*(upper_bound B)*> is FinSequence of REAL by FINSEQ_1:74;
A175: len <*(upper_bound B)*> = 1 by FINSEQ_1:39;
then A176: len (H1 ^ <*(upper_bound B)*>) = (len H1) + 1 by FINSEQ_1:22;
reconsider H = H1 ^ <*(upper_bound B)*> as non empty FinSequence of REAL by A174, FINSEQ_1:75;
for e1, e2 being ExtReal st e1 in dom H & e2 in dom H & e1 < e2 holds
H . e1 < H . e2

proof

let e1, e2 be ExtReal; :: thesis:
assume A177: ( e1 in dom H & e2 in dom H & e1 < e2 ) ; :: thesis:
then A178: ( e1 in Seg (len H) & e2 in Seg (len H) ) by FINSEQ_1:def 3;
reconsider i = e1, j = e2 as Nat by A177;
A179: ( 1 <= i & i <= (len H1) + 1 & 1 <= j & j <= (len H1) + 1 ) by A176, A178, FINSEQ_1:1;

per cases ;

suppose A180: j = (len H1) + 1 ; :: thesis:

then A181: H . e2 = upper_bound B by FINSEQ_1:42;
i <= len H1 by A177, A180, NAT_1:13;
then A182: i in dom H1 by A179, FINSEQ_3:25;
then A183: H . e1 = H1 . i by FINSEQ_1:def 7;
H1 . i in [.(lower_bound B),(S0 . k).] by A122, A182, INTEGRA1:6;
then ex r being Real st
( r = H1 . i & lower_bound B <= r & r <= S0 . k ) ;
hence H . e1 < H . e2 by A5, A168, A181, A183, XXREAL_0:2; :: thesis:

end;

suppose j <> (len H1) + 1 ; :: thesis:

then j < (len H1) + 1 by A179, XXREAL_0:1;
then A184: j <= len H1 by NAT_1:13;
then A185: j in dom H1 by A179, FINSEQ_3:25;
then A186: H . e2 = H1 . j by FINSEQ_1:def 7;
i <= len H1 by A177, A184, XXREAL_0:2;
then A187: i in dom H1 by A179, FINSEQ_3:25;
then H . e1 = H1 . i by FINSEQ_1:def 7;
hence H . e1 < H . e2 by A177, A185, A186, A187, VALUED_0:def 13; :: thesis:

end;

then reconsider H = H as non empty increasing FinSequence of REAL by VALUED_0:def 13;
A188: H . (len H) = upper_bound B by A176, FINSEQ_1:42;
rng H1 c= B1 by INTEGRA1:def 2;
then A189: rng H1 c= B by A123;
A190: rng H = (rng H1) \/ (rng <*(upper_bound B)*>) by FINSEQ_1:31;
A191: rng <*(upper_bound B)*> = {(upper_bound B)} by FINSEQ_1:39;
lower_bound B <= upper_bound B by SEQ_4:11;
then upper_bound B in B by A115;
then rng <*(upper_bound B)*> c= B by A191, ZFMISC_1:31;
then reconsider H = H as Division of B by A188, A189, A190, INTEGRA1:def 2, XBOOLE_1:8;
set F = F1 ^ <*|.(vol ([.(S . k),(upper_bound B).],rho)).|*>;
|.(vol ([.(S . k),(upper_bound B).],rho)).| is Element of REAL by XREAL_0:def 1;
then A192: <*|.(vol ([.(S . k),(upper_bound B).],rho)).|*> is FinSequence of REAL by FINSEQ_1:74;
reconsider F = F1 ^ <*|.(vol ([.(S . k),(upper_bound B).],rho)).|*> as FinSequence of REAL by A192, FINSEQ_1:75;
A193: len F = (len F1) + (len <*|.(vol ([.(S . k),(upper_bound B).],rho)).|*>) by FINSEQ_1:22
.= (len H1) + (len <*|.(vol ([.(S . k),(upper_bound B).],rho)).|*>) by INTEGR22:def 2
.= (len H1) + 1 by FINSEQ_1:40
.= len H by A175, FINSEQ_1:22 ;
1 <= len H1 by NAT_1:14;
then A194: 1 in dom H1 by FINSEQ_3:25;
A195: len F1 = len H1 by INTEGR22:def 2;
then A196: dom F1 = dom H1 by FINSEQ_3:29;
for j being Nat st j in dom H holds
F . j = |.(vol ((divset (H,j)),rho)).|

proof

let j be Nat; :: thesis:
A197: ( divset (H,j) = [.(lower_bound (divset (H,j))),(upper_bound (divset (H,j))).] & divset (H1,j) = [.(lower_bound (divset (H1,j))),(upper_bound (divset (H1,j))).] ) by INTEGRA1:4;
assume A198: j in dom H ; :: thesis:
then A199: ( 1 <= j & j <= len H ) by FINSEQ_3:25;

per cases ;

suppose A200: j = 1 ; :: thesis:

then A201: ( lower_bound (divset (H,j)) = lower_bound B & upper_bound (divset (H,j)) = H . j ) by A198, INTEGRA1:def 4;
A203: ( lower_bound (divset (H1,j)) = lower_bound B1 & upper_bound (divset (H1,j)) = H1 . j ) by A194, A200, INTEGRA1:def 4;
A204: lower_bound B = lower_bound B1 by A122, A137, INTEGRA1:5;
thus F . j = F1 . j by A196, A194, A200, FINSEQ_1:def 7
.= |.(vol ((divset (H1,j)),rho)).| by A200, A194, INTEGR22:def 2
.= |.(vol ((divset (H,j)),rho)).| by A197, A201, A200, A194, A203, A204, FINSEQ_1:def 7 ; :: thesis:

end;

suppose A205: j <> 1 ; :: thesis:

per cases ;

suppose A206: j = len H ; :: thesis:

then A207: j = (len H1) + 1 by A175, FINSEQ_1:22;
A208: F . j = |.(vol ([.(S . k),(upper_bound B).],rho)).| by A176, A195, A206, FINSEQ_1:42;
A209: ( lower_bound (divset (H,j)) = H . (j - 1) & upper_bound (divset (H,j)) = H . j ) by A198, A205, INTEGRA1:def 4;
j - 1 in NAT by A198, INT_1:5, FINSEQ_3:25;
then reconsider j1 = j - 1 as Nat ;
1 < j by A199, A205, XXREAL_0:1;
then 1 - 1 < j1 by XREAL_1:14;
then A210: 1 <= j1 by NAT_1:14;
j - 1 in dom H1 by A207, A210, FINSEQ_3:25;
then H . (j - 1) = H1 . (len H1) by A207, FINSEQ_1:def 7
.= S . k by A126, INTEGRA1:def 2 ;
hence F . j = |.(vol ((divset (H,j)),rho)).| by A197, A206, A208, A209, INTEGRA1:def 2; :: thesis:

end;

suppose j <> len H ; :: thesis:

then j < (len H1) + 1 by A176, A199, XXREAL_0:1;
then L: j <= len H1 by NAT_1:13;
then A211: j in Seg (len H1) by A199;
A212: j in dom H1 by A199, L, FINSEQ_3:25;
then A213: H . j = H1 . j by FINSEQ_1:def 7;
j - 1 in NAT by A198, FINSEQ_3:25, INT_1:5;
then reconsider j1 = j - 1 as Nat ;
1 < j by A199, A205, XXREAL_0:1;
then j - 1 in Seg (len H1) by A211, FINSEQ_3:12;
then j - 1 in dom H1 by FINSEQ_1:def 3;
then A214: H . j1 = H1 . j1 by FINSEQ_1:def 7;
A215: ( lower_bound (divset (H,j)) = H . (j - 1) & upper_bound (divset (H,j)) = H . j ) by A198, A205, INTEGRA1:def 4;
thus F . j = F1 . j by A196, A212, FINSEQ_1:def 7
.= |.(vol ((divset (H1,j)),rho)).| by A212, INTEGR22:def 2
.= |.(vol ((divset (H,j)),rho)).| by A205, A212, A213, A214, A215, INTEGRA1:def 4 ; :: thesis:

end;

then reconsider F = F as var_volume of rho,H by A193, INTEGR22:def 2;
take H ; :: thesis:
take F ; :: thesis:
A217: p . 1 = |.(vol (((divset (T,1)) /\ (divset (S,(k + 1)))),rho)).| by A156, FINSEQ_3:25, A153;
A218: divset (S,(k + 1)) c= B by A167, INTEGRA1:8;
A219: B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:4;
A221: ( lower_bound (divset (T,1)) = lower_bound A & upper_bound (divset (T,1)) = T . 1 ) by INTEGRA1:def 4, A157;
[.(lower_bound B),(upper_bound B).] c= [.(lower_bound (divset (T,1))),(upper_bound (divset (T,1))).] by A4, A173, A221, XXREAL_1:34;
then [.(lower_bound B),(upper_bound B).] c= divset (T,1) by INTEGRA1:4;
then divset (S,(k + 1)) c= divset (T,1) by A218, A219;
then A222: p . 1 = |.(vol ((divset (S,(k + 1))),rho)).| by A217, XBOOLE_1:28;
for i being Nat st i in dom p & i <> 1 holds
p . i = 0

proof

let i be Nat; :: thesis:
assume A223: ( i in dom p & i <> 1 ) ; :: thesis:
then A225: ( 1 <= i & i <= len p ) by FINSEQ_3:25;
then 1 < i by A223, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then A226: 2 - 1 <= i - 1 by XREAL_1:9;
then reconsider i1 = i - 1 as Nat by INT_1:3, ORDINAL1:def 12;
i - 1 <= (len p) - 0 by A225, XREAL_1:13;
then i1 in dom T by A226, FINSEQ_3:25, A153;
then A227: T . 1 <= T . (i - 1) by A157, A226, VALUED_0:def 15;
A228: ( lower_bound (divset (T,i)) = T . (i - 1) & upper_bound (divset (T,i)) = T . i ) by INTEGRA1:def 4, A223, H;
A229: p . i = |.(vol (((divset (T,i)) /\ (divset (S,(k + 1)))),rho)).| by A153, A223, H;
(divset (T,i)) /\ (divset (S,(k + 1))) c= (divset (T,i)) /\ B by A167, INTEGRA1:8, XBOOLE_1:26;
then A230: (divset (T,i)) /\ (divset (S,(k + 1))) c= [.(lower_bound B),(upper_bound B).] /\ [.(lower_bound (divset (T,i))),(upper_bound (divset (T,i))).] by A219, INTEGRA1:4;
[.(lower_bound B),(upper_bound B).] /\ [.(lower_bound (divset (T,i))),(upper_bound (divset (T,i))).] c= [.(upper_bound B),(upper_bound B).] by A173, A227, A228, Th10, XXREAL_0:2;
then (divset (T,i)) /\ (divset (S,(k + 1))) c= [.(upper_bound B),(upper_bound B).] by A230;
hence p . i = 0 by A229, COMPLEX1:44, Th11; :: thesis:

end;

then A231: Sum p = |.(vol ((divset (S,(k + 1))),rho)).| by A153, A156, A222, Th8, FINSEQ_3:25
.= |.(vol ([.(S . k),(upper_bound B).],rho)).| by A4, A5, A159, A170, INTEGRA1:4 ;
thus Sum ST = (Sum F1) + (Sum p) by A150, A152, A153, RVSUM_1:74
.= Sum F by A231, RVSUM_1:74 ; :: thesis:

end;

suppose A232: m <> 1 ; :: thesis:

S: m in Seg (len T) by A160, FINSEQ_1:def 3;
A233: ( 1 <= m & m <= len T ) by A160, FINSEQ_3:25;
then 1 < m by A232, XXREAL_0:1;
then a234: m - 1 in Seg (len T) by FINSEQ_3:12, S;
then A234: m - 1 in dom T by FINSEQ_1:def 3;
then A235: ( 1 <= m - 1 & m - 1 <= len T ) by FINSEQ_3:25;
reconsider m1 = m - 1 as Nat by a234;
LL: m1 in dom T by a234, FINSEQ_1:def 3;
set IDX = { i where i is Nat : ( i in dom T & T . i <= S . k ) } ;
{ i where i is Nat : ( i in dom T & T . i <= S . k ) } c= dom T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { i where i is Nat : ( i in dom T & T . i <= S . k ) } ; :: thesis:
then ex i being Nat st
( x = i & i in dom T & T . i <= S . k ) ;
hence x in dom T ; :: thesis:

end;

then reconsider IDX = { i where i is Nat : ( i in dom T & T . i <= S . k ) } as finite Subset of NAT by XBOOLE_1:1;

per cases ;

suppose A237: IDX = {} ; :: thesis:

A238: for i being Nat st i in dom T holds
S . k < T . i

proof

assume ex i being Nat st
( i in dom T & not S . k < T . i ) ; :: thesis:
then consider i being Nat such that
A239: ( i in dom T & not S . k < T . i ) ;
i in IDX by A239;
hence contradiction by A237; :: thesis:

end;

reconsider TM1 = T | m1 as non empty increasing FinSequence of REAL by Th12, LL;
A240: len TM1 = m1 by A235, FINSEQ_1:59;
then a240: dom TM1 = Seg m1 by FINSEQ_1:def 3;
then A242: TM1 . (len TM1) = T . m1 by FUNCT_1:49, A240, FINSEQ_3:25, A235;
A243: T . m1 < upper_bound B

proof

assume not T . m1 < upper_bound B ; :: thesis:
then A245: m1 in JDX by A234;
m - 1 < m - 0 by XREAL_1:15;
hence contradiction by A245, NAT_1:def 1; :: thesis:

end;

then reconsider TM1B = TM1 ^ <*(upper_bound B)*> as non empty increasing FinSequence of REAL by A242, Th14;
A246: H1 . (len H1) = S . k by A126, INTEGRA1:def 2;
1 in Seg (len TM1) by A235, A240;
then A248: TM1 . 1 = T . 1 by A240, FUNCT_1:49;
1 in dom TM1 by A235, A240, FINSEQ_3:25;
then A249: TM1B . 1 = T . 1 by A248, FINSEQ_1:def 7;
reconsider H = H1 ^ TM1B as non empty increasing FinSequence of REAL by A157, A238, A246, A249, Th13;
A250: rng TM1B = (rng TM1) \/ (rng <*(upper_bound B)*>) by FINSEQ_1:31;
A251: rng <*(upper_bound B)*> = {(upper_bound B)} by FINSEQ_1:39;
A256: rng TM1 c= B

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A252: z in rng TM1 ; :: thesis:
then reconsider x = z as Real ;
x in rng T by A252, RELAT_1:70, TARSKI:def 3;
then x in A by INTEGRA1:def 2, TARSKI:def 3;
then A253: ex r being Real st
( x = r & lower_bound A <= r & r <= upper_bound A ) by A116;
consider i being object such that
A254: ( i in dom TM1 & x = TM1 . i ) by A252, FUNCT_1:def 3;
reconsider i = i as Nat by A254;
A255: ( 1 <= i & i <= len TM1 ) by FINSEQ_3:25, A254;
1 <= len TM1 by A255, XXREAL_0:2;
then len TM1 in dom TM1 by FINSEQ_3:25;
then TM1 . i <= TM1 . (len TM1) by A254, A255, VALUED_0:def 15;
then x <= upper_bound B by A242, A243, A254, XXREAL_0:2;
hence z in B by A4, A115, A253; :: thesis:

end;

lower_bound B <= upper_bound B by SEQ_4:11;
then upper_bound B in B by A115;
then {(upper_bound B)} c= B by ZFMISC_1:31;
then A257: rng TM1B c= B by A250, A251, A256, XBOOLE_1:8;
rng H1 c= B1 by INTEGRA1:def 2;
then rng H1 c= B by A123;
then (rng H1) \/ (rng TM1B) c= B by A257, XBOOLE_1:8;
then A258: rng H c= B by FINSEQ_1:31;
A259: len TM1B = (len TM1) + (len <*(upper_bound B)*>) by FINSEQ_1:22
.= (len TM1) + 1 by FINSEQ_1:40 ;
(len TM1) + 1 in Seg ((len TM1) + 1) by FINSEQ_1:4;
then A260: (len TM1) + 1 in dom TM1B by A259, FINSEQ_1:def 3;
A261: len H = (len H1) + ((len TM1) + 1) by A259, FINSEQ_1:22;
X: 1 in Seg 1 ;
then A262: 1 in dom <*(upper_bound B)*> by FINSEQ_1:38;
H . (len H) = TM1B . ((len TM1) + 1) by A260, A261, FINSEQ_1:def 7
.= <*(upper_bound B)*> . 1 by A262, FINSEQ_1:def 7
.= upper_bound B by FINSEQ_1:40 ;
then reconsider H = H as Division of B by A258, INTEGRA1:def 2;
set q = (p | m1) ^ <*|.(vol ([.(T . m1),(upper_bound B).],rho)).|*>;
rng ((p | m1) ^ <*|.(vol ([.(T . m1),(upper_bound B).],rho)).|*>) c= REAL ;
then reconsider q = (p | m1) ^ <*|.(vol ([.(T . m1),(upper_bound B).],rho)).|*> as FinSequence of REAL by FINSEQ_1:def 4;
A263: len (p | m1) = m1 by A153, A235, FINSEQ_1:59;
A264: len q = (len (p | m1)) + (len <*|.(vol ([.(T . m1),(upper_bound B).],rho)).|*>) by FINSEQ_1:22
.= m1 + 1 by A263, FINSEQ_1:40
.= m ;
A265: 1 in dom <*|.(vol ([.(T . m1),(upper_bound B).],rho)).|*> by FINSEQ_1:38, X;
A266: q . m = q . (m1 + 1)
.= <*|.(vol ([.(T . m1),(upper_bound B).],rho)).|*> . 1 by A263, A265, FINSEQ_1:def 7
.= |.(vol ([.(T . m1),(upper_bound B).],rho)).| by FINSEQ_1:40 ;
A267: for i being Nat st 1 <= i & i <= m1 holds
q . i = |.(vol (((divset (T,i)) /\ (divset (S,(k + 1)))),rho)).|

proof

let i be Nat; :: thesis:
assume A268: ( 1 <= i & i <= m1 ) ; :: thesis:
then A269: i in Seg m1 ;
then A270: i in dom (p | m1) by A263, FINSEQ_1:def 3;
C: i <= len T by A235, A268, XXREAL_0:2;
thus q . i = (p | m1) . i by A270, FINSEQ_1:def 7
.= p . i by A269, FUNCT_1:49
.= |.(vol (((divset (T,i)) /\ (divset (S,(k + 1)))),rho)).| by A153, C, FINSEQ_3:25, A268 ; :: thesis:

end;

reconsider F = F1 ^ q as FinSequence of REAL ;
A272: Sum F = (Sum F1) + (Sum q) by RVSUM_1:75;
A273: len F = (len F1) + (len q) by FINSEQ_1:22;
A274: len H = ((len H1) + m1) + 1 by A240, A261;
A275: 1 <= len H1 by NAT_1:14;
then A276: 1 in dom H1 by FINSEQ_3:25;
A277: len F1 = len H1 by INTEGR22:def 2;
then A278: dom F1 = dom H1 by FINSEQ_3:29;
m - 1 <= m - 0 by XREAL_1:15;
then 1 <= m by A235, XXREAL_0:2;
then A279: m in dom q by A264, FINSEQ_3:25;
for j being Nat st j in dom H holds
F . j = |.(vol ((divset (H,j)),rho)).|

proof

let j be Nat; :: thesis:
A280: ( divset (H,j) = [.(lower_bound (divset (H,j))),(upper_bound (divset (H,j))).] & divset (H1,j) = [.(lower_bound (divset (H1,j))),(upper_bound (divset (H1,j))).] ) by INTEGRA1:4;
assume A281: j in dom H ; :: thesis:
then A282: ( 1 <= j & j <= len H ) by FINSEQ_3:25;

per cases ;

suppose A283: j = 1 ; :: thesis:

then A284: ( lower_bound (divset (H,j)) = lower_bound B & upper_bound (divset (H,j)) = H . j ) by A281, INTEGRA1:def 4;
A285: j in dom H1 by A275, A283, FINSEQ_3:25;
then A286: ( lower_bound (divset (H1,j)) = lower_bound B1 & upper_bound (divset (H1,j)) = H1 . j ) by A283, INTEGRA1:def 4;
A287: lower_bound B = lower_bound B1 by A122, A137, INTEGRA1:5;
thus F . j = F1 . j by A278, A276, A283, FINSEQ_1:def 7
.= |.(vol ((divset (H1,j)),rho)).| by A285, INTEGR22:def 2
.= |.(vol ((divset (H,j)),rho)).| by A280, A284, A285, A286, A287, FINSEQ_1:def 7 ; :: thesis:

end;

suppose A288: j <> 1 ; :: thesis:

per cases ;

suppose A289: j = len H ; :: thesis:

A290: F . j = |.(vol ([.(T . m1),(upper_bound B).],rho)).| by A240, A261, A266, A277, A279, A289, FINSEQ_1:def 7;
A291: ( lower_bound (divset (H,j)) = H . (j - 1) & upper_bound (divset (H,j)) = H . j ) by A281, A288, INTEGRA1:def 4;
j - 1 in NAT by A281, INT_1:5, FINSEQ_3:25;
then reconsider j1 = j - 1 as Nat ;
m - 1 < m - 0 by XREAL_1:15;
then m1 in Seg m by A235;
then A292: m1 in dom TM1B by A240, A259, FINSEQ_1:def 3;
A293: m1 in dom TM1 by A240, A235, FINSEQ_3:25;
H . j1 = TM1B . m1 by A274, A289, A292, FINSEQ_1:def 7
.= TM1 . m1 by A293, FINSEQ_1:def 7
.= T . m1 by a240, A240, FUNCT_1:49, A235, FINSEQ_3:25 ;
hence F . j = |.(vol ((divset (H,j)),rho)).| by A280, A289, A290, A291, INTEGRA1:def 2; :: thesis:

end;

suppose j <> len H ; :: thesis:

then A294: j < (len H1) + m by A240, A261, A282, XXREAL_0:1;

per cases ;

suppose j > len H1 ; :: thesis:

then A295: j - (len H1) > 0 by XREAL_1:50;
then j - (len H1) in NAT by INT_1:3;
then reconsider j1 = j - (len H1) as Nat ;
A296: j1 < ((len H1) + m) - (len H1) by A294, XREAL_1:14;
then j1 + 1 <= m by NAT_1:13;
then A297: (j1 + 1) - 1 <= m - 1 by XREAL_1:13;
A298: 1 <= j1 by A295, NAT_1:14;
then A299: j1 in Seg m by A296;
A300: j1 in dom q by A296, A264, FINSEQ_3:25, A298;
A301: j1 in Seg m1 by A297, A298;
then A302: j1 in dom TM1 by A240, FINSEQ_1:def 3;
A303: F . j = F . ((len H1) + j1)
.= q . j1 by A277, A300, FINSEQ_1:def 7
.= |.(vol (((divset (T,j1)) /\ (divset (S,(k + 1)))),rho)).| by A267, A297, A298 ;
A304: j1 in dom TM1B by A240, A259, A299, FINSEQ_1:def 3;
len TM1 in Seg (len TM1) by FINSEQ_1:3;
then A305: m1 in dom TM1 by A240, FINSEQ_1:def 3;
A306: H . j = H . ((len H1) + j1)
.= TM1B . j1 by A304, FINSEQ_1:def 7
.= TM1 . j1 by A302, FINSEQ_1:def 7
.= T . j1 by A301, FUNCT_1:49 ;
A307: j1 in dom T by A302, RELAT_1:57;
m1 in dom T by A305, RELAT_1:57;
then T . j1 <= T . m1 by A297, A307, VALUED_0:def 15;
then A308: T . j1 <= upper_bound B by A243, XXREAL_0:2;

per cases ;

suppose A309: j1 <> 1 ; :: thesis:

end;

suppose A322: j1 = 1 ; :: thesis:

then A323: ( lower_bound (divset (T,j1)) = lower_bound A & upper_bound (divset (T,j1)) = T . j1 ) by A307, INTEGRA1:def 4;
A324: divset (T,j1) = [.(lower_bound (divset (T,j1))),(upper_bound (divset (T,j1))).] by INTEGRA1:4;
A325: upper_bound (divset (H,j)) = T . j1 by A281, A288, A306, INTEGRA1:def 4
.= upper_bound (divset (T,j1)) by A307, A322, INTEGRA1:def 4 ;
A326: len H1 in dom H1 by A275, FINSEQ_3:25;
A327: lower_bound (divset (H,j)) = H . (((len H1) + j1) - 1) by A281, A288, INTEGRA1:def 4
.= S . k by A246, A322, A326, FINSEQ_1:def 7 ;
(divset (T,j1)) /\ (divset (S,(k + 1))) = [.(S . k),(upper_bound (divset (T,j1))).] by A4, A163, A169, A170, A171, A308, A323, A324, XXREAL_1:143
.= divset (H,j) by A325, A327, INTEGRA1:4 ;
hence F . j = |.(vol ((divset (H,j)),rho)).| by A303; :: thesis:

end;

suppose B: j <= len H1 ; :: thesis:

then A328: j in Seg (len H1) by A282;
A329: j in dom H1 by A282, B, FINSEQ_3:25;
then A330: H . j = H1 . j by FINSEQ_1:def 7;
j - 1 in NAT by A281, INT_1:5, FINSEQ_3:25;
then reconsider j1 = j - 1 as Nat ;
1 < j by A282, A288, XXREAL_0:1;
then j - 1 in Seg (len H1) by A328, FINSEQ_3:12;
then j - 1 in dom H1 by FINSEQ_1:def 3;
then A331: H . j1 = H1 . j1 by FINSEQ_1:def 7;
A332: ( lower_bound (divset (H,j)) = H . (j - 1) & upper_bound (divset (H,j)) = H . j ) by A281, A288, INTEGRA1:def 4;
thus F . j = F1 . j by A278, A329, FINSEQ_1:def 7
.= |.(vol ((divset (H1,j)),rho)).| by A329, INTEGR22:def 2
.= |.(vol ((divset (H,j)),rho)).| by A288, A329, A330, A331, A332, INTEGRA1:def 4 ; :: thesis:

end;

then reconsider F = F as var_volume of rho,H by A240, A261, A264, A273, A277, INTEGR22:def 2;
take H ; :: thesis:
take F ; :: thesis:
Z: dom p = dom T by FINSEQ_3:29, A153;
A333: for i being Nat st i in dom p holds
( ( i <= len q implies p . i = q . i ) & ( len q < i implies p . i = 0 ) )

proof

let i be Nat; :: thesis:
assume A334: i in dom p ; :: thesis:
then A335: ( 1 <= i & i <= len p ) by FINSEQ_3:25;
dom p = dom T by A153, FINSEQ_3:29;
then A336: p . i = |.(vol (((divset (T,i)) /\ (divset (S,(k + 1)))),rho)).| by A153, A334;
thus ( i <= len q implies p . i = q . i ) :: thesis:

proof

assume A337: i <= len q ; :: thesis:
A338: divset (T,i) = [.(lower_bound (divset (T,i))),(upper_bound (divset (T,i))).] by INTEGRA1:4;

per cases ;

suppose i <> m ; :: thesis:

then i < m by A264, A337, XXREAL_0:1;
then i + 1 <= m by NAT_1:13;
then (i + 1) - 1 <= m - 1 by XREAL_1:13;
hence p . i = q . i by A267, A335, A336; :: thesis:

end;

suppose A339: i = m ; :: thesis:

m - 1 < m - 0 by XREAL_1:15;
then A341: ( lower_bound (divset (T,m)) = T . (m - 1) & upper_bound (divset (T,m)) = T . m ) by A235, A160, INTEGRA1:def 4;
A342: lower_bound (divset (S,(k + 1))) < lower_bound (divset (T,m)) by A170, A234, A238, A341;
(divset (T,i)) /\ (divset (S,(k + 1))) = [.(lower_bound (divset (T,i))),(upper_bound (divset (T,i))).] /\ [.(lower_bound (divset (S,(k + 1)))),(upper_bound (divset (S,(k + 1)))).] by A338, INTEGRA1:4
.= [.(T . m1),(upper_bound B).] by A4, A5, A159, A160, A170, A339, A341, A342, XXREAL_1:143 ;
hence p . i = q . i by A153, A266, A334, A339, Z; :: thesis:

end;

A343: divset (T,i) = [.(lower_bound (divset (T,i))),(upper_bound (divset (T,i))).] by INTEGRA1:4;
thus ( len q < i implies p . i = 0 ) :: thesis:

proof

assume A344: len q < i ; :: thesis:
m - 1 < m - 0 by XREAL_1:15;
then A345: 1 < m by A235, XXREAL_0:2;
then A346: ( lower_bound (divset (T,i)) = T . (i - 1) & upper_bound (divset (T,i)) = T . i ) by A264, A344, INTEGRA1:def 4, A334, Z;
m + 1 <= i by A264, A344, NAT_1:13;
then A347: (m + 1) - 1 <= i - 1 by XREAL_1:13;
then A348: 1 < i - 1 by A345, XXREAL_0:2;
i - 1 in NAT by A347, INT_1:3;
then reconsider i1 = i - 1 as Nat ;
(len T) - 1 < (len T) - 0 by XREAL_1:15;
then i1 <= len T by A153, A335, XREAL_1:15;
then A350: i1 in dom T by A348, FINSEQ_3:25;
(divset (T,i)) /\ (divset (S,(k + 1))) c= [.(upper_bound (divset (S,(k + 1)))),(upper_bound (divset (S,(k + 1)))).] by A4, A5, A159, A164, A169, A170, A343, A346, A347, A350, Th10;
hence p . i = 0 by A336, COMPLEX1:44, Th11; :: thesis:

end;

thus Sum ST = (Sum F1) + (Sum p) by A150, A152, A153, RVSUM_1:74
.= Sum F by A272, A264, A153, A160, FINSEQ_3:25, A333, Th9 ; :: thesis:

end;

suppose IDX <> {} ; :: thesis:

then A351: sup IDX in IDX by XXREAL_2:def 6;
then reconsider n = sup IDX as Nat ;
consider i being Nat such that
A352: ( n = i & i in dom T & T . i <= S . k ) by A351;
A353: ( 1 <= n & n <= len T ) by FINSEQ_3:25, A352;
n <> len T

proof

assume n = len T ; :: thesis:
then A354: upper_bound A <= S . k by A352, INTEGRA1:def 2;
upper_bound A < upper_bound B by A168, A354, XXREAL_0:2;
hence contradiction by A4, XXREAL_2:59; :: thesis:

end;

then n < len T by A353, XXREAL_0:1;
then Z: ( 1 <= n + 1 & n + 1 <= len T ) by NAT_1:11, NAT_1:13;
then A355: n + 1 in dom T by FINSEQ_3:25;
A356: S . k < T . (n + 1)

proof

assume T . (n + 1) <= S . k ; :: thesis:
then n + 1 in IDX by A355;
hence contradiction by NAT_1:16, XXREAL_2:4; :: thesis:

end;

A357: for i being Nat st i in dom T & n < i holds
S . k < T . i

proof

let i be Nat; :: thesis:
assume A358: ( i in dom T & n < i ) ; :: thesis:
then A359: n + 1 <= i by NAT_1:13;
n + 1 in dom T by Z, FINSEQ_3:25;
then T . (n + 1) <= T . i by A358, A359, VALUED_0:def 15;
hence S . k < T . i by A356, XXREAL_0:2; :: thesis:

end;

A361: n < m

proof

assume m <= n ; :: thesis:
then T . m <= T . n by A160, A352, VALUED_0:def 15;
then upper_bound B <= T . n by A160, XXREAL_0:2;
hence contradiction by A168, A352, XXREAL_0:2; :: thesis:

end;

A364: for i being Nat st i <= n & i in dom T holds
T . i <= S . k

proof

let i be Nat; :: thesis:
assume A365: ( i <= n & i in dom T ) ; :: thesis:
assume A366: not T . i <= S . k ; :: thesis:
T . i <= T . n by A352, A365, VALUED_0:def 15;
hence contradiction by A352, A366, XXREAL_0:2; :: thesis:

end;

A368: for i being Nat st n < i & i < m & i in dom T holds
( S . k < T . i & T . i < S . (k + 1) )

proof

let i be Nat; :: thesis:
assume A369: ( n < i & i < m & i in dom T ) ; :: thesis:
hence S . k < T . i by A357; :: thesis:
assume not T . i < S . (k + 1) ; :: thesis:
then i in JDX by A4, A5, A159, A369;
hence contradiction by A369, NAT_1:def 1; :: thesis:

end;

A370: n + 1 <= m by A361, NAT_1:13;

per cases ;

suppose A371: n + 1 = m ; :: thesis:

set H = H1 ^ <*(upper_bound B)*>;
H1 . (len H1) = S . k by A126, INTEGRA1:def 2;
then reconsider H = H1 ^ <*(upper_bound B)*> as non empty increasing FinSequence of REAL by A168, Th14;
A372: len <*(upper_bound B)*> = 1 by FINSEQ_1:39;
then A373: len H = (len H1) + 1 by FINSEQ_1:22;
A374: H . (len H) = upper_bound B by A373, FINSEQ_1:42;
rng H1 c= B1 by INTEGRA1:def 2;
then A375: rng H1 c= B by A123;
A376: rng H = (rng H1) \/ (rng <*(upper_bound B)*>) by FINSEQ_1:31;
A377: rng <*(upper_bound B)*> = {(upper_bound B)} by FINSEQ_1:39;
lower_bound B <= upper_bound B by SEQ_4:11;
then upper_bound B in B by A115;
then rng <*(upper_bound B)*> c= B by A377, ZFMISC_1:31;
then reconsider H = H as Division of B by A374, A375, A376, INTEGRA1:def 2, XBOOLE_1:8;
set F = F1 ^ <*|.(vol ([.(S . k),(upper_bound B).],rho)).|*>;
|.(vol ([.(S . k),(upper_bound B).],rho)).| is Element of REAL by XREAL_0:def 1;
then A378: <*|.(vol ([.(S . k),(upper_bound B).],rho)).|*> is FinSequence of REAL by FINSEQ_1:74;
reconsider F = F1 ^ <*|.(vol ([.(S . k),(upper_bound B).],rho)).|*> as FinSequence of REAL by A378, FINSEQ_1:75;
A379: len F = (len F1) + (len <*|.(vol ([.(S . k),(upper_bound B).],rho)).|*>) by FINSEQ_1:22
.= (len H1) + (len <*|.(vol ([.(S . k),(upper_bound B).],rho)).|*>) by INTEGR22:def 2
.= (len H1) + 1 by FINSEQ_1:40
.= len H by A372, FINSEQ_1:22 ;
D: 1 <= len H1 by NAT_1:14;
then A380: 1 in dom H1 by FINSEQ_3:25;
A381: len F1 = len H1 by INTEGR22:def 2;
then A382: dom F1 = dom H1 by FINSEQ_3:29;
for j being Nat st j in dom H holds
F . j = |.(vol ((divset (H,j)),rho)).|

proof

let j be Nat; :: thesis:
A383: ( divset (H,j) = [.(lower_bound (divset (H,j))),(upper_bound (divset (H,j))).] & divset (H1,j) = [.(lower_bound (divset (H1,j))),(upper_bound (divset (H1,j))).] ) by INTEGRA1:4;
assume A384: j in dom H ; :: thesis:
then A385: ( 1 <= j & j <= len H ) by FINSEQ_3:25;

per cases ;

suppose A386: j = 1 ; :: thesis:

then A387: ( lower_bound (divset (H,j)) = lower_bound B & upper_bound (divset (H,j)) = H . j ) by A384, INTEGRA1:def 4;
A388: j in dom H1 by D, A386, FINSEQ_3:25;
A389: ( lower_bound (divset (H1,j)) = lower_bound B1 & upper_bound (divset (H1,j)) = H1 . j ) by INTEGRA1:def 4, A380, A386;
A390: lower_bound B = lower_bound B1 by A122, A137, INTEGRA1:5;
thus F . j = F1 . j by A382, A388, FINSEQ_1:def 7
.= |.(vol ((divset (H1,j)),rho)).| by A388, INTEGR22:def 2
.= |.(vol ((divset (H,j)),rho)).| by A383, A387, A388, A389, A390, FINSEQ_1:def 7 ; :: thesis:

end;

suppose A391: j <> 1 ; :: thesis:

per cases ;

suppose A392: j = len H ; :: thesis:

A393: F . j = |.(vol ([.(S . k),(upper_bound B).],rho)).| by A373, A381, A392, FINSEQ_1:42;
A394: ( lower_bound (divset (H,j)) = H . (j - 1) & upper_bound (divset (H,j)) = H . j ) by A384, A391, INTEGRA1:def 4;
j - 1 in NAT by A384, INT_1:5, FINSEQ_3:25;
then reconsider j1 = j - 1 as Nat ;
1 < j by A385, A391, XXREAL_0:1;
then 1 - 1 < j1 by XREAL_1:14;
then 1 <= j1 by NAT_1:14;
then j1 in dom H1 by FINSEQ_3:25, A373, A392;
then H . (j - 1) = H1 . (len H1) by A373, A392, FINSEQ_1:def 7
.= S . k by A126, INTEGRA1:def 2 ;
hence F . j = |.(vol ((divset (H,j)),rho)).| by A383, A392, A393, A394, INTEGRA1:def 2; :: thesis:

end;

suppose j <> len H ; :: thesis:

then j < (len H1) + 1 by A373, A385, XXREAL_0:1;
then K: j <= len H1 by NAT_1:13;
then A396: j in Seg (len H1) by A385;
A397: j in dom H1 by FINSEQ_3:25, K, A385;
then A398: H . j = H1 . j by FINSEQ_1:def 7;
j - 1 in NAT by A384, FINSEQ_3:25, INT_1:5;
then reconsider j1 = j - 1 as Nat ;
1 < j by A385, A391, XXREAL_0:1;
then j - 1 in Seg (len H1) by A396, FINSEQ_3:12;
then j - 1 in dom H1 by FINSEQ_1:def 3;
then A399: H . j1 = H1 . j1 by FINSEQ_1:def 7;
A400: ( lower_bound (divset (H,j)) = H . (j - 1) & upper_bound (divset (H,j)) = H . j ) by A384, A391, INTEGRA1:def 4;
thus F . j = F1 . j by A382, A397, FINSEQ_1:def 7
.= |.(vol ((divset (H1,j)),rho)).| by A397, INTEGR22:def 2
.= |.(vol ((divset (H,j)),rho)).| by A391, A397, A398, A399, A400, INTEGRA1:def 4 ; :: thesis:

end;

then reconsider F = F as var_volume of rho,H by A379, INTEGR22:def 2;
take H ; :: thesis:
take F ; :: thesis:
A401: 1 < 1 + n by A353, NAT_1:16;
A403: p . m = |.(vol (((divset (T,m)) /\ (divset (S,(k + 1)))),rho)).| by A153, A160;
A405: ( lower_bound (divset (T,m)) = T . m1 & upper_bound (divset (T,m)) = T . m ) by A160, A371, A401, INTEGRA1:def 4;
[.(lower_bound (divset (S,(k + 1)))),(upper_bound (divset (S,(k + 1)))).] c= [.(lower_bound (divset (T,m))),(upper_bound (divset (T,m))).] by A160, A170, A171, A352, A371, A405, XXREAL_1:34;
then divset (S,(k + 1)) c= divset (T,m) by A169, INTEGRA1:4;
then A406: p . m = |.(vol ((divset (S,(k + 1))),rho)).| by A403, XBOOLE_1:28;
for i being Nat st i in dom p & i <> m holds
p . i = 0

proof

let i be Nat; :: thesis:
assume A407: ( i in dom p & i <> m ) ; :: thesis:
then A408: i in Seg (len p) by FINSEQ_1:def 3;
A409: ( 1 <= i & i <= len p ) by A407, FINSEQ_3:25;

per cases by A407, XXREAL_0:1;

suppose A410: i < m ; :: thesis:

A412: i in dom T by A153, A408, FINSEQ_1:def 3;
A413: upper_bound (divset (T,i)) = T . i

proof

per cases ;

suppose i = 1 ; :: thesis:

hence upper_bound (divset (T,i)) = T . i by A412, INTEGRA1:def 4; :: thesis:

end;

suppose i <> 1 ; :: thesis:

hence upper_bound (divset (T,i)) = T . i by A412, INTEGRA1:def 4; :: thesis:

end;

A414: (i + 1) - 1 <= (n + 1) - 1 by A371, A410, NAT_1:13;
A415: (divset (T,i)) /\ (divset (S,(k + 1))) = [.(lower_bound (divset (T,i))),(upper_bound (divset (T,i))).] /\ [.(lower_bound (divset (S,(k + 1)))),(upper_bound (divset (S,(k + 1)))).] by A169, INTEGRA1:4;
(divset (T,i)) /\ (divset (S,(k + 1))) c= [.(upper_bound (divset (T,i))),(upper_bound (divset (T,i))).] by H, A170, A364, A407, A413, A414, A415, Th10;
then vol (((divset (T,i)) /\ (divset (S,(k + 1)))),rho) = 0 by Th11;
hence p . i = 0 by A153, COMPLEX1:44, A412; :: thesis:

end;

suppose A416: m < i ; :: thesis:

then A417: 1 < i by A353, A371, NAT_1:16, XXREAL_0:2;
a418: i in dom T by A153, A408, FINSEQ_1:def 3;
then A419: ( lower_bound (divset (T,i)) = T . (i - 1) & upper_bound (divset (T,i)) = T . i ) by A371, A401, A416, INTEGRA1:def 4;
m + 1 <= i by A416, NAT_1:13;
then A420: (m + 1) - 1 <= i - 1 by XREAL_1:9;
1 + 1 <= i by A417, NAT_1:13;
then A421: 2 - 1 <= i - 1 by XREAL_1:9;
then reconsider i1 = i - 1 as Nat by INT_1:3, ORDINAL1:def 12;
i - 1 <= (len p) - 0 by A409, XREAL_1:13;
then i1 in dom T by A153, FINSEQ_3:25, A421;
then A422: T . m <= T . i1 by A160, A420, VALUED_0:def 15;
(divset (T,i)) /\ (divset (S,(k + 1))) = [.(lower_bound (divset (T,i))),(upper_bound (divset (T,i))).] /\ [.(lower_bound (divset (S,(k + 1)))),(upper_bound (divset (S,(k + 1)))).] by A169, INTEGRA1:4;
then (divset (T,i)) /\ (divset (S,(k + 1))) c= [.(upper_bound (divset (S,(k + 1)))),(upper_bound (divset (S,(k + 1)))).] by A160, A170, A171, A419, A422, Th10, XXREAL_0:2;
then vol (((divset (T,i)) /\ (divset (S,(k + 1)))),rho) = 0 by Th11;
hence p . i = 0 by A153, a418, COMPLEX1:44; :: thesis:

end;

then A423: Sum p = |.(vol ((divset (S,(k + 1))),rho)).| by A160, H, A406, Th8
.= |.(vol ([.(S . k),(upper_bound B).],rho)).| by A4, A5, A159, A170, INTEGRA1:4 ;
thus Sum ST = (Sum F1) + (Sum p) by A150, A152, A153, RVSUM_1:74
.= Sum F by A423, RVSUM_1:74 ; :: thesis:

end;

suppose A424: n + 1 <> m ; :: thesis:

then A425: n + 1 < m by A370, XXREAL_0:1;
m - (n + 1) in NAT by A370, INT_1:5;
then reconsider mn1 = m - (n + 1) as Nat ;
m - n in NAT by A361, INT_1:5;
then reconsider mn = m - n as Nat ;
A426: 0 + 1 <= mn1 by A425, NAT_1:13, XREAL_1:50;
(m - n) - 1 <= mn - 0 by XREAL_1:13;
then A427: 1 <= mn by A426, XXREAL_0:2;
consider TM1 being non empty increasing FinSequence of REAL such that
A428: ( len TM1 = mn1 & rng TM1 c= rng T & ( for i being Nat st i in dom TM1 holds
TM1 . i = T . (i + n) ) ) by A233, A425, Th16;
consider pM1 being FinSequence of REAL such that
A429: ( len pM1 = mn1 - 1 & rng pM1 c= rng p & ( for i being Nat st i in dom pM1 holds
pM1 . i = p . ((i + n) + 1) ) ) by A153, A233, A425, Th17;
reconsider m1 = m - 1 as Nat by a234;
A430: TM1 . (len TM1) = T . (mn1 + n) by FINSEQ_3:25, A426, A428;
A431: T . (mn1 + n) < upper_bound B

proof

assume A432: not T . (mn1 + n) < upper_bound B ; :: thesis:
A433: mn1 + n in JDX by A234, A432;
m - 1 < m - 0 by XREAL_1:15;
hence contradiction by A433, NAT_1:def 1; :: thesis:

end;

then reconsider TM1B = TM1 ^ <*(upper_bound B)*> as non empty increasing FinSequence of REAL by A430, Th14;
A434: H1 . (len H1) = S . k by A126, INTEGRA1:def 2;
KK: 1 in dom TM1 by A426, A428, FINSEQ_3:25;
A436: TM1 . 1 = T . (1 + n) by A428, A426, FINSEQ_3:25;
A437: TM1B . 1 = T . (1 + n) by A436, FINSEQ_1:def 7, KK;
reconsider H = H1 ^ TM1B as non empty increasing FinSequence of REAL by A356, A434, A437, Th13;
A438: rng TM1B = (rng TM1) \/ (rng <*(upper_bound B)*>) by FINSEQ_1:31;
A439: rng <*(upper_bound B)*> = {(upper_bound B)} by FINSEQ_1:39;
A444: rng TM1 c= B

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A440: z in rng TM1 ; :: thesis:
then reconsider x = z as Real ;
x in A by A428, A440, INTEGRA1:def 2, TARSKI:def 3;
then A441: ex r being Real st
( x = r & lower_bound A <= r & r <= upper_bound A ) by A116;
consider i being object such that
A442: ( i in dom TM1 & x = TM1 . i ) by A440, FUNCT_1:def 3;
reconsider i = i as Nat by A442;
A443: ( 1 <= i & i <= len TM1 ) by A442, FINSEQ_3:25;
( 1 <= len TM1 & len TM1 <= len TM1 ) by A443, XXREAL_0:2;
then len TM1 in dom TM1 by FINSEQ_3:25;
then TM1 . i <= TM1 . (len TM1) by A442, A443, VALUED_0:def 15;
then x <= upper_bound B by A430, A431, A442, XXREAL_0:2;
hence z in B by A4, A115, A441; :: thesis:

end;

lower_bound B <= upper_bound B by SEQ_4:11;
then upper_bound B in B by A115;
then {(upper_bound B)} c= B by ZFMISC_1:31;
then A445: rng TM1B c= B by A438, A439, A444, XBOOLE_1:8;
rng H1 c= B1 by INTEGRA1:def 2;
then rng H1 c= B by A123;
then (rng H1) \/ (rng TM1B) c= B by A445, XBOOLE_1:8;
then A446: rng H c= B by FINSEQ_1:31;
A447: len TM1B = (len TM1) + (len <*(upper_bound B)*>) by FINSEQ_1:22
.= (len TM1) + 1 by FINSEQ_1:40 ;
(len TM1) + 1 in Seg ((len TM1) + 1) by FINSEQ_1:4;
then A448: (len TM1) + 1 in dom TM1B by A447, FINSEQ_1:def 3;
A449: len H = (len H1) + ((len TM1) + 1) by A447, FINSEQ_1:22;
G: 1 in Seg 1 ;
then A450: 1 in dom <*(upper_bound B)*> by FINSEQ_1:38;
H . (len H) = TM1B . ((len TM1) + 1) by A448, A449, FINSEQ_1:def 7
.= <*(upper_bound B)*> . 1 by A450, FINSEQ_1:def 7
.= upper_bound B by FINSEQ_1:40 ;
then reconsider H = H as Division of B by A446, INTEGRA1:def 2;
set q1 = <*|.(vol ([.(S . k),(T . (n + 1)).],rho)).|*> ^ pM1;
set q = (<*|.(vol ([.(S . k),(T . (n + 1)).],rho)).|*> ^ pM1) ^ <*|.(vol ([.(T . m1),(upper_bound B).],rho)).|*>;
rng (<*|.(vol ([.(S . k),(T . (n + 1)).],rho)).|*> ^ pM1) c= REAL ;
then reconsider q1 = <*|.(vol ([.(S . k),(T . (n + 1)).],rho)).|*> ^ pM1 as FinSequence of REAL by FINSEQ_1:def 4;
rng ((<*|.(vol ([.(S . k),(T . (n + 1)).],rho)).|*> ^ pM1) ^ <*|.(vol ([.(T . m1),(upper_bound B).],rho)).|*>) c= REAL ;
then reconsider q = (<*|.(vol ([.(S . k),(T . (n + 1)).],rho)).|*> ^ pM1) ^ <*|.(vol ([.(T . m1),(upper_bound B).],rho)).|*> as FinSequence of REAL by FINSEQ_1:def 4;
A451: len q1 = (len <*|.(vol ([.(S . k),(T . (n + 1)).],rho)).|*>) + (len pM1) by FINSEQ_1:22
.= 1 + (mn1 - 1) by A429, FINSEQ_1:40
.= mn1 ;
A452: len q = (len q1) + (len <*|.(vol ([.(T . m1),(upper_bound B).],rho)).|*>) by FINSEQ_1:22
.= mn1 + 1 by A451, FINSEQ_1:40
.= mn ;
A453: 1 in dom <*|.(vol ([.(T . m1),(upper_bound B).],rho)).|*> by G, FINSEQ_1:38;
A454: q . (len q) = q . (mn1 + 1) by A452
.= <*|.(vol ([.(T . m1),(upper_bound B).],rho)).|*> . 1 by A451, A453, FINSEQ_1:def 7
.= |.(vol ([.(T . m1),(upper_bound B).],rho)).| by FINSEQ_1:40 ;
A455: 1 in dom <*|.(vol ([.(S . k),(T . (n + 1)).],rho)).|*> by FINSEQ_1:38, G;
1 in Seg mn1 by A426;
then 1 in dom q1 by A451, FINSEQ_1:def 3;
then A456: q . 1 = q1 . 1 by FINSEQ_1:def 7
.= <*|.(vol ([.(S . k),(T . (n + 1)).],rho)).|*> . 1 by A455, FINSEQ_1:def 7
.= |.(vol ([.(S . k),(T . (n + 1)).],rho)).| by FINSEQ_1:40 ;
A457: for i being Nat st 2 <= i & i <= len q1 holds
q . i = |.(vol (((divset (T,(n + i))) /\ (divset (S,(k + 1)))),rho)).|

proof

let i be Nat; :: thesis:
assume A458: ( 2 <= i & i <= len q1 ) ; :: thesis:
then A459: 1 <= i by XXREAL_0:2;
then i in dom q1 by A458, FINSEQ_3:25;
then A460: q . i = q1 . i by FINSEQ_1:def 7;
A461: 2 - 1 <= i - 1 by A458, XREAL_1:9;
then A462: ( 1 <= i - 1 & i - 1 <= mn1 - 1 ) by A451, A458, XREAL_1:9;
i - 1 in NAT by A461, INT_1:3;
then reconsider i1 = i - 1 as Nat ;
A463: len <*|.(vol ([.(S . k),(T . (n + 1)).],rho)).|*> = 1 by FINSEQ_1:40;
A465: i1 in dom pM1 by FINSEQ_3:25, A429, A462;
A466: q1 . i = q1 . (1 + i1)
.= pM1 . i1 by A463, A465, FINSEQ_1:def 7
.= p . ((i1 + n) + 1) by FINSEQ_3:25, A429, A462
.= p . (i + n) ;
i <= i + n by NAT_1:11;
then A467: 1 <= i + n by A459, XXREAL_0:2;
i + n <= ((m - n) - 1) + n by A451, A458, XREAL_1:6;
then i + n <= len T by A235, XXREAL_0:2;
hence q . i = |.(vol (((divset (T,(n + i))) /\ (divset (S,(k + 1)))),rho)).| by A153, A460, A466, FINSEQ_3:25, A467; :: thesis:

end;

reconsider F = F1 ^ q as FinSequence of REAL ;
A468: len F = (len F1) + (len q) by FINSEQ_1:22;
E: 1 <= len H1 by NAT_1:14;
then A469: 1 in dom H1 by FINSEQ_3:25;
A470: len F1 = len H1 by INTEGR22:def 2;
then A471: dom F1 = dom H1 by FINSEQ_3:29;
mn in Seg mn by A427;
then A472: mn in dom q by A452, FINSEQ_1:def 3;
1 <= len q by NAT_1:14;
then A473: 1 in dom q by FINSEQ_3:25;
1 <= len TM1B by NAT_1:14;
then A474: 1 in dom TM1B by FINSEQ_3:25;
1 <= len TM1 by NAT_1:14;
then A475: 1 in dom TM1 by FINSEQ_3:25;
A476: H . ((len H1) + 1) = TM1B . 1 by A474, FINSEQ_1:def 7
.= TM1 . 1 by A475, FINSEQ_1:def 7
.= T . (n + 1) by A428, A426, FINSEQ_3:25 ;
for j being Nat st j in dom H holds
F . j = |.(vol ((divset (H,j)),rho)).|

proof

let j be Nat; :: thesis:
A477: ( divset (H,j) = [.(lower_bound (divset (H,j))),(upper_bound (divset (H,j))).] & divset (H1,j) = [.(lower_bound (divset (H1,j))),(upper_bound (divset (H1,j))).] ) by INTEGRA1:4;
assume A478: j in dom H ; :: thesis:
then A479: ( 1 <= j & j <= len H ) by FINSEQ_3:25;

per cases ;

suppose A480: j = 1 ; :: thesis:

then A481: ( lower_bound (divset (H,j)) = lower_bound B & upper_bound (divset (H,j)) = H . j ) by A478, INTEGRA1:def 4;
A482: j in dom H1 by E, A480, FINSEQ_3:25;
A483: ( lower_bound (divset (H1,j)) = lower_bound B1 & upper_bound (divset (H1,j)) = H1 . j ) by A469, A480, INTEGRA1:def 4;
A484: lower_bound B = lower_bound B1 by A122, A137, INTEGRA1:5;
thus F . j = F1 . j by A471, A482, FINSEQ_1:def 7
.= |.(vol ((divset (H1,j)),rho)).| by A482, INTEGR22:def 2
.= |.(vol ((divset (H,j)),rho)).| by A477, A481, A482, A483, A484, FINSEQ_1:def 7 ; :: thesis:

end;

suppose A485: j <> 1 ; :: thesis:

per cases ;

suppose A486: j = len H ; :: thesis:

then A487: j = ((len H1) + mn1) + 1 by A428, A449;
A488: F . j = |.(vol ([.(T . m1),(upper_bound B).],rho)).| by A428, A449, A452, A454, A470, A472, A486, FINSEQ_1:def 7;
A489: ( lower_bound (divset (H,j)) = H . (j - 1) & upper_bound (divset (H,j)) = H . j ) by A478, A485, INTEGRA1:def 4;
j - 1 in NAT by A478, INT_1:5, FINSEQ_3:25;
then reconsider j1 = j - 1 as Nat ;
mn - 1 < mn - 0 by XREAL_1:15;
then mn1 in Seg mn by A426;
then A490: mn1 in dom TM1B by A428, A447, FINSEQ_1:def 3;
len TM1 in Seg (len TM1) by FINSEQ_1:3;
then A491: mn1 in dom TM1 by A428, FINSEQ_1:def 3;
H . j1 = TM1B . mn1 by A487, A490, FINSEQ_1:def 7
.= T . m1 by A428, A430, A491, FINSEQ_1:def 7 ;
hence F . j = |.(vol ((divset (H,j)),rho)).| by A477, A486, A488, A489, INTEGRA1:def 2; :: thesis:

end;

suppose j <> len H ; :: thesis:

then A492: j < ((len H1) + mn1) + 1 by A428, A449, A479, XXREAL_0:1;

per cases ;

suppose j > len H1 ; :: thesis:

then A493: j - (len H1) > 0 by XREAL_1:50;
then j - (len H1) in NAT by INT_1:3;
then reconsider j1 = j - (len H1) as Nat ;
A494: j1 < ((len H1) + mn) - (len H1) by A492, XREAL_1:14;
then j1 + 1 <= mn by NAT_1:13;
then A495: (j1 + 1) - 1 <= mn - 1 by XREAL_1:13;
A496: 1 <= j1 by A493, NAT_1:14;
then A497: j1 in Seg mn by A494;
then A498: j1 in dom q by A452, FINSEQ_1:def 3;
( 1 <= j1 & j1 <= mn1 ) by A493, A495, NAT_1:14;
then j1 in Seg mn1 ;
then A500: j1 in dom TM1 by A428, FINSEQ_1:def 3;
A501: j1 in dom TM1B by A428, A447, A497, FINSEQ_1:def 3;
A502: H . j = H . ((len H1) + j1)
.= TM1B . j1 by A501, FINSEQ_1:def 7
.= TM1 . j1 by A500, FINSEQ_1:def 7
.= T . (j1 + n) by A428, A500 ;
A503: j1 + n <= mn1 + n by A495, XREAL_1:6;
A504: 1 <= j1 + n by A493, NAT_1:14;
j1 + n <= len T by A235, A503, XXREAL_0:2;
then A505: j1 + n in dom T by A504, FINSEQ_3:25;
then T . (j1 + n) <= T . (mn1 + n) by A234, A503, VALUED_0:def 15;
then A506: T . (j1 + n) <= upper_bound (divset (S,(k + 1))) by A4, A5, A159, A170, A431, XXREAL_0:2;

per cases ;

suppose A507: j1 = 1 ; :: thesis:

0 < len H1 ;
then 1 + 0 < 1 + (len H1) by XREAL_1:8;
then A508: ( lower_bound (divset (H,j)) = H . (j - 1) & upper_bound (divset (H,j)) = H . j ) by A478, A507, INTEGRA1:def 4;
len H1 in Seg (len H1) by FINSEQ_1:3;
then A509: len H1 in dom H1 by FINSEQ_1:def 3;
A510: F . j = F . ((len H1) + 1) by A507
.= |.(vol ([.(S . k),(T . (n + 1)).],rho)).| by A456, A470, A473, FINSEQ_1:def 7 ;
H . (len H1) = S . k by A434, A509, FINSEQ_1:def 7;
hence F . j = |.(vol ((divset (H,j)),rho)).| by A476, A507, A508, A510, INTEGRA1:4; :: thesis:

end;

suppose j1 <> 1 ; :: thesis:

then A511: 1 < j1 by A496, XXREAL_0:1;
then A512: 1 + 1 <= j1 by NAT_1:13;
A513: F . j = F . ((len H1) + j1)
.= q . j1 by A470, A498, FINSEQ_1:def 7
.= |.(vol (((divset (T,(j1 + n))) /\ (divset (S,(k + 1)))),rho)).| by A451, A457, A495, A512 ;
A514: j1 + n <> 1 by A511, NAT_1:11;
then 1 < j1 + n by A504, XXREAL_0:1;
then 1 + 1 <= j1 + n by NAT_1:13;
then A515: (1 + 1) - 1 <= (j1 + n) - 1 by XREAL_1:9;
then (j1 + n) - 1 in NAT by INT_1:3;
then reconsider j11 = (j1 + n) - 1 as Nat ;
2 + (n - 1) <= j1 + (n - 1) by A512, XREAL_1:6;
then n + 1 <= j11 ;
then A516: n < j11 by NAT_1:16, XXREAL_0:2;
A517: j1 + (n - 1) <= ((m - n) - 1) + (n - 1) by A495, XREAL_1:6;
m1 - 1 <= m1 - 0 by XREAL_1:13;
then A518: j11 <= m1 by A517, XXREAL_0:2;
j11 <= len T by A235, A518, XXREAL_0:2;
then j11 in dom T by FINSEQ_3:25, A515;
then A519: S . k < T . j11 by A357, A516;
A520: lower_bound (divset (S,(k + 1))) <= lower_bound (divset (T,(j1 + n))) by A170, A505, A514, A519, INTEGRA1:def 4;
A521: upper_bound (divset (T,(j1 + n))) <= upper_bound (divset (S,(k + 1))) by A505, A506, A514, INTEGRA1:def 4;
A522: divset (T,(j1 + n)) = [.(lower_bound (divset (T,(j1 + n)))),(upper_bound (divset (T,(j1 + n)))).] by INTEGRA1:4;
A523: (divset (T,(j1 + n))) /\ (divset (S,(k + 1))) = divset (T,(j1 + n)) by A169, A520, A521, A522, XBOOLE_1:28, XXREAL_1:34;
j1 - 1 <= j1 - 0 by XREAL_1:13;
then A524: j11 - n <= mn1 by A495, XXREAL_0:2;
A525: 2 - 1 <= j1 - 1 by A512, XREAL_1:9;
then j11 - n in NAT by INT_1:3;
then reconsider j11n = j11 - n as Nat ;
j11n in Seg mn1 by A524, A525;
then A527: j11 - n in dom TM1 by A428, FINSEQ_1:def 3;
mn - 1 <= mn - 0 by XREAL_1:13;
then ( 1 <= j11 - n & j11 - n <= mn ) by A524, A525, XXREAL_0:2;
then j11n in Seg mn ;
then A528: j11 - n in dom TM1B by A428, A447, FINSEQ_1:def 3;
A529: H . (j - 1) = H . ((len H1) + (j11 - n))
.= TM1B . (j11 - n) by A528, FINSEQ_1:def 7
.= TM1 . (j11 - n) by A527, FINSEQ_1:def 7
.= T . ((j1 - 1) + n) by A428, A527 ;
A530: upper_bound (divset (H,j)) = T . (j1 + n) by A478, A485, A502, INTEGRA1:def 4
.= upper_bound (divset (T,(j1 + n))) by A505, A514, INTEGRA1:def 4 ;
lower_bound (divset (H,j)) = T . ((j1 + n) - 1) by A478, A485, A529, INTEGRA1:def 4
.= lower_bound (divset (T,(j1 + n))) by A505, A514, INTEGRA1:def 4 ;
hence F . j = |.(vol ((divset (H,j)),rho)).| by A513, A522, A523, A530, INTEGRA1:4; :: thesis:

end;

suppose j <= len H1 ; :: thesis:

then A531: j in Seg (len H1) by A479;
then A532: j in dom H1 by FINSEQ_1:def 3;
then A533: H . j = H1 . j by FINSEQ_1:def 7;
j - 1 in NAT by A478, INT_1:5, FINSEQ_3:25;
then reconsider j1 = j - 1 as Nat ;
1 < j by A479, A485, XXREAL_0:1;
then j - 1 in Seg (len H1) by A531, FINSEQ_3:12;
then j - 1 in dom H1 by FINSEQ_1:def 3;
then A534: H . j1 = H1 . j1 by FINSEQ_1:def 7;
A535: ( lower_bound (divset (H,j)) = H . (j - 1) & upper_bound (divset (H,j)) = H . j ) by A478, A485, INTEGRA1:def 4;
thus F . j = F1 . j by A471, A532, FINSEQ_1:def 7
.= |.(vol ((divset (H1,j)),rho)).| by A532, INTEGR22:def 2
.= |.(vol ((divset (H,j)),rho)).| by A485, A532, A533, A534, A535, INTEGRA1:def 4 ; :: thesis:

end;

then reconsider F = F as var_volume of rho,H by A428, A449, A452, A468, A470, INTEGR22:def 2;
take H ; :: thesis:
take F ; :: thesis:
A536: for i being Nat st i in dom p holds
( ( i <= n implies p . i = 0 ) & ( i <= len q implies p . (n + i) = q . i ) & ( (len q) + n < i implies p . i = 0 ) )

proof

let i be Nat; :: thesis:
assume A537: i in dom p ; :: thesis:
then A538: ( 1 <= i & i <= len p ) by FINSEQ_3:25;
F: dom p = dom T by A153, FINSEQ_3:29;
then A539: p . i = |.(vol (((divset (T,i)) /\ (divset (S,(k + 1)))),rho)).| by A153, A537;
thus ( i <= n implies p . i = 0 ) :: thesis:

proof

assume A540: i <= n ; :: thesis:

per cases ;

suppose i = 1 ; :: thesis:

then A542: ( lower_bound (divset (T,i)) = lower_bound A & upper_bound (divset (T,i)) = T . i ) by INTEGRA1:def 4, F, A537;
(divset (T,i)) /\ (divset (S,(k + 1))) = [.(lower_bound (divset (T,i))),(upper_bound (divset (T,i))).] /\ [.(lower_bound (divset (S,(k + 1)))),(upper_bound (divset (S,(k + 1)))).] by A169, INTEGRA1:4;
then (divset (T,i)) /\ (divset (S,(k + 1))) c= [.(upper_bound (divset (T,i))),(upper_bound (divset (T,i))).] by A170, A364, A537, A540, F, A542, Th10;
hence p . i = 0 by A539, COMPLEX1:44, Th11; :: thesis:

end;

suppose A543: i <> 1 ; :: thesis:

then 1 < i by A538, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then (1 + 1) - 1 <= i - 1 by XREAL_1:13;
then i - 1 in NAT by INT_1:3;
then reconsider i1 = i - 1 as Nat ;
A544: ( lower_bound (divset (T,i)) = T . (i - 1) & upper_bound (divset (T,i)) = T . i ) by A543, INTEGRA1:def 4, A537, F;
(divset (T,i)) /\ (divset (S,(k + 1))) = [.(lower_bound (divset (T,i))),(upper_bound (divset (T,i))).] /\ [.(lower_bound (divset (S,(k + 1)))),(upper_bound (divset (S,(k + 1)))).] by A169, INTEGRA1:4;
then (divset (T,i)) /\ (divset (S,(k + 1))) c= [.(upper_bound (divset (T,i))),(upper_bound (divset (T,i))).] by A170, A364, A537, A540, A544, F, Th10;
hence p . i = 0 by A539, COMPLEX1:44, Th11; :: thesis:

end;

thus ( i <= len q implies p . (n + i) = q . i ) :: thesis:

proof

assume A545: i <= len q ; :: thesis:

per cases ;

suppose A546: i = 1 ; :: thesis:

A547: divset (T,(n + 1)) = [.(lower_bound (divset (T,(n + 1)))),(upper_bound (divset (T,(n + 1)))).] by INTEGRA1:4;
n <> 0 by FINSEQ_3:25, A352;
then A548: n + 1 <> 1 ;
A549: ( lower_bound (divset (T,(n + 1))) = T . ((n + 1) - 1) & upper_bound (divset (T,(n + 1))) = T . (n + 1) ) by A548, A355, INTEGRA1:def 4;
( n < n + 1 & n + 1 < m ) by A370, A424, NAT_1:16, XXREAL_0:1;
then A550: T . (n + 1) < S . (k + 1) by A355, A368;
(divset (T,(n + 1))) /\ (divset (S,(k + 1))) = [.(S . k),(T . (n + 1)).] by A169, A170, A352, A547, A549, A550, XXREAL_1:143;
hence p . (n + i) = q . i by A153, Z, A456, A546, FINSEQ_3:25; :: thesis:

end;

suppose i <> 1 ; :: thesis:

then 1 < i by A538, XXREAL_0:1;
then A551: 1 + 1 <= i by NAT_1:13;

per cases ;

suppose i <> mn ; :: thesis:

then i < mn by A452, A545, XXREAL_0:1;
then i + 1 <= mn by NAT_1:13;
then (i + 1) - 1 <= mn - 1 by XREAL_1:9;
then A552: q . i = |.(vol (((divset (T,(n + i))) /\ (divset (S,(k + 1)))),rho)).| by A451, A457, A551;
i + n <= (m - n) + n by A452, A545, XREAL_1:7;
then A553: i + n <= len T by A233, XXREAL_0:2;
1 + 0 <= i + n by A538, XREAL_1:7;
then n + i in Seg (len T) by A553;
then n + i in dom T by FINSEQ_1:def 3;
hence p . (n + i) = q . i by A153, A552; :: thesis:

end;

suppose A554: i = mn ; :: thesis:

1 <= n + 1 by NAT_1:11;
then A556: ( lower_bound (divset (T,m)) = T . (m - 1) & upper_bound (divset (T,m)) = T . m ) by A425, A160, INTEGRA1:def 4;
A557: m - 1 < m - 0 by XREAL_1:15;
(n + 1) - 1 < m - 1 by A425, XREAL_1:14;
then A558: ( S . k < T . m1 & T . m1 < S . (k + 1) ) by A234, A368, A557;
(divset (T,m)) /\ (divset (S,(k + 1))) = [.(lower_bound (divset (T,m))),(upper_bound (divset (T,m))).] /\ [.(lower_bound (divset (S,(k + 1)))),(upper_bound (divset (S,(k + 1)))).] by A169, INTEGRA1:4
.= [.(T . m1),(upper_bound B).] by A4, A5, A159, A160, A170, A556, A558, XXREAL_1:143 ;
hence p . (n + i) = q . i by A153, A160, A452, A454, A554; :: thesis:

end;

thus ( (len q) + n < i implies p . i = 0 ) :: thesis:

proof

assume A559: (len q) + n < i ; :: thesis:
m - 1 < m - 0 by XREAL_1:15;
then A560: 1 < m by A235, XXREAL_0:2;
A561: ( lower_bound (divset (T,i)) = T . (i - 1) & upper_bound (divset (T,i)) = T . i ) by A452, A559, A560, INTEGRA1:def 4, A537, F;
m + 1 <= i by A452, A559, NAT_1:13;
then A562: (m + 1) - 1 <= i - 1 by XREAL_1:13;
then A563: 1 < i - 1 by A560, XXREAL_0:2;
i - 1 in NAT by A562, INT_1:3;
then reconsider i1 = i - 1 as Nat ;
(len T) - 1 < (len T) - 0 by XREAL_1:15;
then A565: i1 in dom T by A563, FINSEQ_3:25, A153, A538, XREAL_1:13;
(divset (T,i)) /\ (divset (S,(k + 1))) = [.(lower_bound (divset (T,i))),(upper_bound (divset (T,i))).] /\ [.(lower_bound (divset (S,(k + 1)))),(upper_bound (divset (S,(k + 1)))).] by A169, INTEGRA1:4;
then (divset (T,i)) /\ (divset (S,(k + 1))) c= [.(upper_bound (divset (S,(k + 1)))),(upper_bound (divset (S,(k + 1)))).] by A4, A5, A159, A164, A170, A561, A562, A565, Th10;
hence p . i = 0 by A539, COMPLEX1:44, Th11; :: thesis:

end;

(len p) - ((len q) + n) in NAT by A153, A233, A452, INT_1:5;
then reconsider L = (len p) - ((len q) + n) as Nat ;
set s = ((n |-> 0) ^ q) ^ (L |-> 0);
reconsider nn = n, nL = L as Element of NAT by ORDINAL1:def 12;
reconsider z0 = 0 as Element of REAL by XREAL_0:def 1;
A566: len (n |-> 0) = len (nn |-> z0)
.= n by FINSEQ_2:133 ;
A567: len (L |-> 0) = len (nL |-> z0)
.= L by FINSEQ_2:133 ;
A568: len (((n |-> 0) ^ q) ^ (L |-> 0)) = (len ((n |-> 0) ^ q)) + (len (L |-> 0)) by FINSEQ_1:22
.= (n + (len q)) + L by A566, A567, FINSEQ_1:22
.= len p ;
for j being Nat st 1 <= j & j <= len p holds
p . j = (((n |-> 0) ^ q) ^ (L |-> 0)) . j

proof

let j be Nat; :: thesis:
assume A569: ( 1 <= j & j <= len p ) ; :: thesis:
then A570: j in dom p by FINSEQ_3:25;
set sw = (n |-> 0) ^ q;
A571: len ((n |-> 0) ^ q) = n + (len q) by A566, FINSEQ_1:22;

per cases ;

suppose A572: j <= n ; :: thesis:

then A573: p . j = 0 by A536, A570;
j <= n + (len q) by A572, NAT_1:12;
then j in Seg (len ((n |-> 0) ^ q)) by A569, A571;
then j in dom ((n |-> 0) ^ q) by FINSEQ_1:def 3;
then A574: (((n |-> 0) ^ q) ^ (L |-> 0)) . j = ((n |-> 0) ^ q) . j by FINSEQ_1:def 7;
j in Seg (len (n |-> 0)) by A566, A569, A572;
then j in dom (n |-> 0) by FINSEQ_1:def 3;
then A575: ((n |-> 0) ^ q) . j = (n |-> 0) . j by FINSEQ_1:def 7;
j in Seg n by A569, A572;
hence p . j = (((n |-> 0) ^ q) ^ (L |-> 0)) . j by A573, A574, A575, FINSEQ_2:57; :: thesis:

end;

suppose A576: n < j ; :: thesis:

per cases ;

suppose A577: j <= (len q) + n ; :: thesis:

j - n in NAT by A576, INT_1:5;
then reconsider jn = j - n as Nat ;
A578: 0 + 1 <= jn by A576, NAT_1:13, XREAL_1:50;
A579: j - n <= ((len q) + n) - n by A577, XREAL_1:9;
then A580: jn in dom q by A578, FINSEQ_3:25;
len q <= (len q) + n by NAT_1:11;
then len q <= len p by A153, A233, A452, XXREAL_0:2;
then jn <= len p by A579, XXREAL_0:2;
then jn in dom p by FINSEQ_3:25, A578;
then A581: p . (n + jn) = q . jn by A536, A579;
A582: j in dom ((n |-> 0) ^ q) by A569, A571, A577, FINSEQ_3:25;
(((n |-> 0) ^ q) ^ (L |-> 0)) . j = ((n |-> 0) ^ q) . (n + jn) by A582, FINSEQ_1:def 7
.= q . jn by A566, A580, FINSEQ_1:def 7 ;
hence p . j = (((n |-> 0) ^ q) ^ (L |-> 0)) . j by A581; :: thesis:

end;

suppose A583: (len q) + n < j ; :: thesis:

j - ((len q) + n) in NAT by A583, INT_1:5;
then reconsider j1 = j - ((len q) + n) as Nat ;
A584: 0 + 1 <= j1 by A583, NAT_1:13, XREAL_1:50;
j - ((len q) + n) <= (len p) - ((len q) + n) by A569, XREAL_1:9;
then A585: j1 in Seg L by A584;
then A586: j1 in dom (L |-> 0) by A567, FINSEQ_1:def 3;
(((n |-> 0) ^ q) ^ (L |-> 0)) . j = (((n |-> 0) ^ q) ^ (L |-> 0)) . ((len ((n |-> 0) ^ q)) + j1) by A571
.= (L |-> 0) . j1 by A586, FINSEQ_1:def 7
.= 0 by A585, FINSEQ_2:57 ;
hence p . j = (((n |-> 0) ^ q) ^ (L |-> 0)) . j by A536, A570, A583; :: thesis:

end;

then A587: p = ((n |-> 0) ^ q) ^ (L |-> 0) by A568;
A588: Sum p = (Sum ((n |-> 0) ^ q)) + (Sum (L |-> 0)) by A587, RVSUM_1:75
.= ((Sum (n |-> 0)) + (Sum q)) + (Sum (L |-> 0)) by RVSUM_1:75
.= (0 + (Sum q)) + (Sum (L |-> 0)) by RVSUM_1:81
.= 0 + (Sum q) by RVSUM_1:81 ;
thus Sum ST = (Sum F1) + (Sum p) by A150, A152, A153, RVSUM_1:74
.= Sum F by A588, RVSUM_1:75 ; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence for B being non empty closed_interval Subset of REAL
for S0 being non empty increasing FinSequence of REAL
for ST being FinSequence of REAL st B c= A & lower_bound B = lower_bound A & ex S being Division of B st
( S = S0 & len ST = len S & ( for j being Nat st j in dom S holds
ex p being FinSequence of REAL st
( ST . j = Sum p & len p = len T & ( for i being Nat st i in dom T holds
p . i = |.(vol (((divset (T,i)) /\ (divset (S,j))),rho)).| ) ) ) ) holds
ex H being Division of B ex F being var_volume of rho,H st Sum ST = Sum F ; :: thesis: