let f be PartFunc of REAL,REAL; :: thesis: for a, b, c being Real st a < b & b < c & ['a,c'] c= dom f & f | ['a,b'] is bounded & f | ['b,c'] is bounded & f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] holds
f is_integrable_on ['a,c']
let a, b, c be Real; :: thesis: ( a < b & b < c & ['a,c'] c= dom f & f | ['a,b'] is bounded & f | ['b,c'] is bounded & f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] implies f is_integrable_on ['a,c'] )
assume that
A1: ( a < b & b < c ) and
A2: ['a,c'] c= dom f and
A3: f | ['a,b'] is bounded and
A4: f | ['b,c'] is bounded and
A5: f is_integrable_on ['a,b'] and
A6: f is_integrable_on ['b,c'] ; :: thesis: f is_integrable_on ['a,c']
set AB = ['a,b'];
set BC = ['b,c'];
set AC = ['a,c'];
set F1 = f || ['a,b'];
set F2 = f || ['b,c'];
A7: (f || ['a,c']) | ['a,c'] = f | ['a,c'] ;
dom (f | ['a,c']) = ['a,c'] by A2, RELAT_1:62;
then A8: f || ['a,c'] is Function of ['a,c'],REAL by FUNCT_2:def 1;
A9: ( ['a,b'] = [.a,b.] & ['b,c'] = [.b,c.] & ['a,c'] = [.a,c.] ) by A1, INTEGRA5:def 3, XXREAL_0:2;
then A10: ['a,b'] \/ ['b,c'] = ['a,c'] by A1, XXREAL_1:165;
then f | ['a,c'] is bounded by A3, A4, RFUNCT_1:87;
then A11: ( f || ['a,c'] is upper_integrable & f || ['a,c'] is lower_integrable ) by A7, A8, INTEGRA4:10;
A12: ( ['b,c'] c= ['a,c'] & ['a,b'] c= ['a,c'] ) by A1, A9, XXREAL_1:34;
then ( ['b,c'] c= dom f & ['a,b'] c= dom f ) by A2;
then ( dom (f | ['b,c']) = ['b,c'] & dom (f | ['a,b']) = ['a,b'] ) by RELAT_1:62;
then A13: ( f || ['b,c'] is Function of ['b,c'],REAL & f || ['a,b'] is Function of ['a,b'],REAL ) by FUNCT_2:def 1;
( [.b,c.] = [.(lower_bound [.b,c.]),(upper_bound [.b,c.]).] & [.a,b.] = [.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] & [.a,c.] = [.(lower_bound [.a,c.]),(upper_bound [.a,c.]).] ) by A9, INTEGRA1:4;
then A14: ( upper_bound ['b,c'] = c & lower_bound ['b,c'] = b & upper_bound ['a,b'] = b & lower_bound ['a,b'] = a & upper_bound ['a,c'] = c & lower_bound ['a,c'] = a ) by A9, INTEGRA1:5;
vol ['b,c'] = (upper_bound ['b,c']) - (lower_bound ['b,c']) by INTEGRA1:def 5;
then consider PS2 being DivSequence of ['b,c'] such that
A15: ( delta PS2 is convergent & lim (delta PS2) = 0 ) and
A16: for n being Element of NAT ex Tn being Division of ['b,c'] st
( Tn divide_into_equal n + 1 & PS2 . n = Tn ) by A1, A14, XREAL_1:50, INTEGRA6:16;
A17: for i being Element of NAT st 2 <= i holds
ex S2i being Division of ['b,c'] st
( S2i = PS2 . i & 2 <= len S2i )
proof
let i be Element of NAT ; :: thesis: ( 2 <= i implies ex S2i being Division of ['b,c'] st
( S2i = PS2 . i & 2 <= len S2i ) )
assume A18: 2 <= i ; :: thesis: ex S2i being Division of ['b,c'] st
( S2i = PS2 . i & 2 <= len S2i )
consider Tn being Division of ['b,c'] such that
A19: Tn divide_into_equal i + 1 and
A20: PS2 . i = Tn by A16;
reconsider Tn = Tn as Division of ['b,c'] ;
take Tn ; :: thesis: ( Tn = PS2 . i & 2 <= len Tn )
thus Tn = PS2 . i by A20; :: thesis: 2 <= len Tn
len Tn = i + 1 by A19, INTEGRA4:def 1;
then i <= len Tn by NAT_1:11;
hence 2 <= len Tn by A18, XXREAL_0:2; :: thesis: verum
end;
defpred S1[ set , set ] means ex n being Element of NAT ex e being Division of ['b,c'] st
( n = $1 & e = $2 & e = PS2 . (n + 2) );
A21: for n being Element of NAT ex D being Element of divs ['b,c'] st S1[n,D]
proof
let n be Element of NAT ; :: thesis: ex D being Element of divs ['b,c'] st S1[n,D]
reconsider D = PS2 . (n + 2) as Element of divs ['b,c'] by INTEGRA1:def 3;
take D ; :: thesis: S1[n,D]
thus S1[n,D] ; :: thesis: verum
end;
consider S2 being sequence of (divs ['b,c']) such that
A22: for n being Element of NAT holds S1[n,S2 . n] from FUNCT_2:sch 3(A21);
 reconsider S2 = S2 as DivSequence of ['b,c'] ;
defpred S2[ Element of NAT , set ] means ex S being Division of ['b,c'] st
( S = S2 . $1 & $2 = S /^ 1 );
A23: now :: thesis: for i being Element of NAT ex S2i being Division of ['b,c'] st
( S2i = S2 . i & 2 <= len S2i )
let i be Element of NAT ; :: thesis: ex S2i being Division of ['b,c'] st
( S2i = S2 . i & 2 <= len S2i )
ex n being Element of NAT ex e being Division of ['b,c'] st
( n = i & e = S2 . i & e = PS2 . (n + 2) ) by A22;
hence ex S2i being Division of ['b,c'] st
( S2i = S2 . i & 2 <= len S2i ) by A17, NAT_1:11; :: thesis: verum
end;
A24: for i being Element of NAT ex T being Element of divs ['b,c'] st S2[i,T]
proof
let i be Element of NAT ; :: thesis: ex T being Element of divs ['b,c'] st S2[i,T]
consider S being Division of ['b,c'] such that
A25: S = S2 . i and
A26: 2 <= len S by A23;
set T = S /^ 1;
A27: 1 <= len S by A26, XXREAL_0:2;
2 - 1 <= (len S) - 1 by A26, XREAL_1:13;
then A28: 1 <= len (S /^ 1) by A27, RFINSEQ:def 1;
then len (S /^ 1) in dom (S /^ 1) by FINSEQ_3:25;
then (S /^ 1) . (len (S /^ 1)) = S . ((len (S /^ 1)) + 1) by A27, RFINSEQ:def 1;
then (S /^ 1) . (len (S /^ 1)) = S . (((len S) - 1) + 1) by A27, RFINSEQ:def 1;
then A29: (S /^ 1) . (len (S /^ 1)) = upper_bound ['b,c'] by INTEGRA1:def 2;
( rng S c= ['b,c'] & rng (S /^ 1) c= rng S ) by FINSEQ_5:33, INTEGRA1:def 2;
then A30: rng (S /^ 1) c= ['b,c'] ;
( not S /^ 1 is empty & S /^ 1 is increasing ) by A26, A28, INTEGRA1:34, XXREAL_0:2;
then S /^ 1 is Division of ['b,c'] by A30, A29, INTEGRA1:def 2;
then S /^ 1 is Element of divs ['b,c'] by INTEGRA1:def 3;
hence ex T being Element of divs ['b,c'] st S2[i,T] by A25; :: thesis: verum
end;
consider T2 being DivSequence of ['b,c'] such that
A31: for i being Element of NAT holds S2[i,T2 . i] from FUNCT_2:sch 3(A24);
 A32: for n being Element of NAT ex D being Division of ['b,c'] st
( D = T2 . n & ( for i being Element of NAT st i in dom D holds
b < D . i ) )
proof
let n be Element of NAT ; :: thesis: ex D being Division of ['b,c'] st
( D = T2 . n & ( for i being Element of NAT st i in dom D holds
b < D . i ) )
reconsider D = T2 . n as Division of ['b,c'] ;
take D ; :: thesis: ( D = T2 . n & ( for i being Element of NAT st i in dom D holds
b < D . i ) )
consider E being Division of ['b,c'] such that
A33: E = S2 . n and
A34: T2 . n = E /^ 1 by A31;
A35: ex E1 being Division of ['b,c'] st
( E1 = S2 . n & 2 <= len E1 ) by A23;
then A36: 2 - 1 <= (len E) - 1 by A33, XREAL_1:13;
A37: 1 <= len E by A33, A35, XXREAL_0:2;
then 1 in Seg (len E) by FINSEQ_1:1;
then A38: 1 in dom E by FINSEQ_1:def 3;
then ( rng E c= ['b,c'] & E . 1 in rng E ) by FUNCT_1:def 3, INTEGRA1:def 2;
then A39: b <= E . 1 by A9, XXREAL_1:1;
2 in Seg (len E) by A33, A35, FINSEQ_1:1;
then 2 in dom E by FINSEQ_1:def 3;
then A40: E . 1 < E . 2 by A38, SEQM_3:def 1;
len D = (len E) - 1 by A34, A37, RFINSEQ:def 1;
then 1 in Seg (len D) by A36, FINSEQ_1:1;
then A41: 1 in dom D by FINSEQ_1:def 3;
then A42: D . 1 = E . (1 + 1) by A34, A37, RFINSEQ:def 1;
then A43: b < D . 1 by A39, A40, XXREAL_0:2;
now :: thesis: for i being Element of NAT st i in dom D holds
( ( i <> 1 implies b < D . i ) & b < D . i )
let i be Element of NAT ; :: thesis: ( i in dom D implies ( ( i <> 1 implies b < D . i ) & b < D . i ) )
assume A44: i in dom D ; :: thesis: ( ( i <> 1 implies b < D . i ) & b < D . i )
then A45: 1 <= i by FINSEQ_3:25;
hereby :: thesis: b < D . i
assume i <> 1 ; :: thesis: b < D . i
then 1 < i by A45, XXREAL_0:1;
then D . 1 < D . i by A41, A44, SEQM_3:def 1;
hence b < D . i by A43, XXREAL_0:2; :: thesis: verum
end;
hence b < D . i by A42, A39, A40, XXREAL_0:2; :: thesis: verum
end;
hence ( D = T2 . n & ( for i being Element of NAT st i in dom D holds
b < D . i ) ) ; :: thesis: verum
end;
consider T1 being DivSequence of ['a,b'] such that
A46: ( delta T1 is convergent & lim (delta T1) = 0 ) by INTEGRA4:11;
A47: for n being Element of NAT ex D being Division of ['b,c'] st
( D = T2 . n & 1 <= len D )
proof
let n be Element of NAT ; :: thesis: ex D being Division of ['b,c'] st
( D = T2 . n & 1 <= len D )
reconsider D = T2 . n as Division of ['b,c'] ;
take D ; :: thesis: ( D = T2 . n & 1 <= len D )
consider E being Division of ['b,c'] such that
A48: E = S2 . n and
A49: T2 . n = E /^ 1 by A31;
ex E1 being Division of ['b,c'] st
( E1 = S2 . n & 2 <= len E1 ) by A23;
then ( 1 <= len E & 2 - 1 <= (len E) - 1 ) by A48, XREAL_1:13, XXREAL_0:2;
hence ( D = T2 . n & 1 <= len D ) by A49, RFINSEQ:def 1; :: thesis: verum
end;
defpred S3[ Element of NAT , set ] means ex S1 being Division of ['a,b'] ex S2 being Division of ['b,c'] st
( S1 = T1 . $1 & S2 = T2 . $1 & $2 = S1 ^ S2 );
A50: for i being Element of NAT ex T being Element of divs ['a,c'] st S3[i,T]
proof
let i0 be Element of NAT ; :: thesis: ex T being Element of divs ['a,c'] st S3[i0,T]
reconsider S1 = T1 . i0 as Division of ['a,b'] ;
reconsider S2 = T2 . i0 as Division of ['b,c'] ;
set T = S1 ^ S2;
ex D being Division of ['b,c'] st
( D = T2 . i0 & 1 <= len D ) by A47;
then len S2 in Seg (len S2) by FINSEQ_1:1;
then A51: len S2 in dom S2 by FINSEQ_1:def 3;
A52: rng S1 c= ['a,b'] by INTEGRA1:def 2;
now :: thesis: for i, j being Nat st i in dom (S1 ^ S2) & j in dom (S1 ^ S2) & i < j holds
(S1 ^ S2) . i < (S1 ^ S2) . j
let i, j be Nat; :: thesis: ( i in dom (S1 ^ S2) & j in dom (S1 ^ S2) & i < j implies (S1 ^ S2) . i < (S1 ^ S2) . j )
assume that
A53: i in dom (S1 ^ S2) and
A54: j in dom (S1 ^ S2) and
A55: i < j ; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
A56: 1 <= i by A53, FINSEQ_3:25;
A57: j <= len (S1 ^ S2) by A54, FINSEQ_3:25;
A58: i <= len (S1 ^ S2) by A53, FINSEQ_3:25;
A59: now :: thesis: ( j > len S1 implies (S1 ^ S2) . i < (S1 ^ S2) . j )
j <= (len S1) + (len S2) by A57, FINSEQ_1:22;
then A60: j - (len S1) <= len S2 by XREAL_1:20;
assume A61: j > len S1 ; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
then A62: (S1 ^ S2) . j = S2 . (j - (len S1)) by A57, FINSEQ_1:24;
A63: (len S1) + 1 <= j by A61, NAT_1:13;
then consider m being Nat such that
A64: ((len S1) + 1) + m = j by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
1 + m = j - (len S1) by A64;
then 1 <= 1 + m by A63, XREAL_1:19;
then 1 + m in Seg (len S2) by A64, A60, FINSEQ_1:1;
then A65: j - (len S1) in dom S2 by A64, FINSEQ_1:def 3;
A66: now :: thesis: ( i > len S1 implies (S1 ^ S2) . i < (S1 ^ S2) . j )
i <= (len S1) + (len S2) by A58, FINSEQ_1:22;
then A67: i - (len S1) <= len S2 by XREAL_1:20;
A68: i - (len S1) < j - (len S1) by A55, XREAL_1:14;
assume A69: i > len S1 ; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
then A70: (len S1) + 1 <= i by NAT_1:13;
then consider m being Nat such that
A71: ((len S1) + 1) + m = i by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
1 + m = i - (len S1) by A71;
then 1 <= 1 + m by A70, XREAL_1:19;
then 1 + m in Seg (len S2) by A71, A67, FINSEQ_1:1;
then A72: i - (len S1) in dom S2 by A71, FINSEQ_1:def 3;
(S1 ^ S2) . i = S2 . (i - (len S1)) by A58, A69, FINSEQ_1:24;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A62, A65, A68, A72, SEQM_3:def 1; :: thesis: verum
end;
now :: thesis: ( i <= len S1 implies (S1 ^ S2) . i < (S1 ^ S2) . j )
assume i <= len S1 ; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
then A73: i in dom S1 by A56, FINSEQ_3:25;
then (S1 ^ S2) . i = S1 . i by FINSEQ_1:def 7;
then (S1 ^ S2) . i in rng S1 by A73, FUNCT_1:def 3;
then A74: (S1 ^ S2) . i <= b by A9, A52, XXREAL_1:1;
ex DD being Division of ['b,c'] st
( DD = T2 . i0 & ( for k being Element of NAT st k in dom DD holds
b < DD . k ) ) by A32;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A62, A65, A74, XXREAL_0:2; :: thesis: verum
end;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A66; :: thesis: verum
end;
A75: 1 <= j by A54, FINSEQ_3:25;
now :: thesis: ( j <= len S1 implies (S1 ^ S2) . i < (S1 ^ S2) . j )
assume A76: j <= len S1 ; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
then A77: j in dom S1 by A75, FINSEQ_3:25;
then A78: (S1 ^ S2) . j = S1 . j by FINSEQ_1:def 7;
i <= len S1 by A55, A76, XXREAL_0:2;
then A79: i in dom S1 by A56, FINSEQ_3:25;
then (S1 ^ S2) . i = S1 . i by FINSEQ_1:def 7;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A55, A79, A77, A78, SEQM_3:def 1; :: thesis: verum
end;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A59; :: thesis: verum
end;
then A80: S1 ^ S2 is non empty increasing FinSequence of REAL by SEQM_3:def 1;
rng S2 c= ['b,c'] by INTEGRA1:def 2;
then (rng S1) \/ (rng S2) c= ['a,b'] \/ ['b,c'] by A52, XBOOLE_1:13;
then (rng S1) \/ (rng S2) c= ['a,c'] by A1, A9, XXREAL_1:174;
then A81: rng (S1 ^ S2) c= ['a,c'] by FINSEQ_1:31;
(S1 ^ S2) . (len (S1 ^ S2)) = (S1 ^ S2) . ((len S1) + (len S2)) by FINSEQ_1:22
.= S2 . (len S2) by A51, FINSEQ_1:def 7
.= upper_bound ['a,c'] by A14, INTEGRA1:def 2 ;
then S1 ^ S2 is Division of ['a,c'] by A81, A80, INTEGRA1:def 2;
then S1 ^ S2 is Element of divs ['a,c'] by INTEGRA1:def 3;
hence ex T being Element of divs ['a,c'] st S3[i0,T] ; :: thesis: verum
end;
consider T being DivSequence of ['a,c'] such that
A82: for i being Element of NAT holds S3[i,T . i] from FUNCT_2:sch 3(A50);
 A83: for i, k being Element of NAT
for S0 being Division of ['a,b'] st S0 = T1 . i & k in Seg (len S0) holds
divset ((T . i),k) = divset ((T1 . i),k)
proof
let i, k be Element of NAT ; :: thesis: for S0 being Division of ['a,b'] st S0 = T1 . i & k in Seg (len S0) holds
divset ((T . i),k) = divset ((T1 . i),k)
let S0 be Division of ['a,b']; :: thesis: ( S0 = T1 . i & k in Seg (len S0) implies divset ((T . i),k) = divset ((T1 . i),k) )
assume A84: S0 = T1 . i ; :: thesis: ( not k in Seg (len S0) or divset ((T . i),k) = divset ((T1 . i),k) )
reconsider S = T . i as Division of ['a,c'] ;
A85: divset ((T1 . i),k) = [.(lower_bound (divset ((T1 . i),k))),(upper_bound (divset ((T1 . i),k))).] by INTEGRA1:4;
consider S1 being Division of ['a,b'], S2 being Division of ['b,c'] such that
A86: S1 = T1 . i and
S2 = T2 . i and
A87: T . i = S1 ^ S2 by A82;
assume A88: k in Seg (len S0) ; :: thesis: divset ((T . i),k) = divset ((T1 . i),k)
then A89: k in dom S1 by A84, A86, FINSEQ_1:def 3;
len S = (len S1) + (len S2) by A87, FINSEQ_1:22;
then Seg (len S1) c= Seg (len S) by NAT_1:11, FINSEQ_1:5;
then k in Seg (len S) by A84, A88, A86;
then A90: k in dom S by FINSEQ_1:def 3;
A91: divset ((T . i),k) = [.(lower_bound (divset ((T . i),k))),(upper_bound (divset ((T . i),k))).] by INTEGRA1:4;
A92: now :: thesis: ( k <> 1 implies divset ((T . i),k) = divset ((T1 . i),k) )
( k <= len S1 & k - 1 <= k - 0 ) by A84, A88, A86, FINSEQ_1:1, XREAL_1:10;
then A93: k - 1 <= len S1 by XXREAL_0:2;
assume A94: k <> 1 ; :: thesis: divset ((T . i),k) = divset ((T1 . i),k)
1 <= k by A88, FINSEQ_1:1;
then A95: 1 < k by A94, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
then A96: 2 - 1 <= k - 1 by XREAL_1:9;
k - 1 is Element of NAT by A95, NAT_1:20;
then k - 1 in Seg (len S1) by A93, A96, FINSEQ_1:1;
then A97: k - 1 in dom S1 by FINSEQ_1:def 3;
thus divset ((T . i),k) = [.(S . (k - 1)),(upper_bound (divset ((T . i),k))).] by A90, A91, A94, INTEGRA1:def 4
.= [.(S . (k - 1)),(S . k).] by A90, A94, INTEGRA1:def 4
.= [.(S . (k - 1)),(S1 . k).] by A87, A89, FINSEQ_1:def 7
.= [.(S1 . (k - 1)),(S1 . k).] by A87, A97, FINSEQ_1:def 7
.= [.(lower_bound (divset ((T1 . i),k))),(S1 . k).] by A86, A89, A94, INTEGRA1:def 4
.= divset ((T1 . i),k) by A86, A89, A85, A94, INTEGRA1:def 4 ; :: thesis: verum
end;
now :: thesis: ( k = 1 implies divset ((T . i),k) = divset ((T1 . i),k) )
assume A98: k = 1 ; :: thesis: divset ((T . i),k) = divset ((T1 . i),k)
hence divset ((T . i),k) = [.(lower_bound ['a,c']),(upper_bound (divset ((T . i),k))).] by A90, A91, INTEGRA1:def 4
.= [.(lower_bound ['a,c']),(S . k).] by A90, A98, INTEGRA1:def 4
.= [.(lower_bound ['a,c']),(S1 . k).] by A87, A89, FINSEQ_1:def 7
.= [.(lower_bound (divset ((T1 . i),k))),(S1 . 1).] by A14, A86, A89, A98, INTEGRA1:def 4
.= divset ((T1 . i),k) by A86, A89, A85, A98, INTEGRA1:def 4 ;
:: thesis: verum
end;
hence divset ((T . i),k) = divset ((T1 . i),k) by A92; :: thesis: verum
end;
A99: for i, k being Element of NAT
for S01 being Division of ['a,b']
for S02 being Division of ['b,c'] st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds
divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)
proof
let i, k be Element of NAT ; :: thesis: for S01 being Division of ['a,b']
for S02 being Division of ['b,c'] st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds
divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)
let S01 be Division of ['a,b']; :: thesis: for S02 being Division of ['b,c'] st S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) holds
divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)
let S02 be Division of ['b,c']; :: thesis: ( S01 = T1 . i & S02 = T2 . i & k in Seg (len S02) implies divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) )
assume that
A100: S01 = T1 . i and
A101: S02 = T2 . i ; :: thesis: ( not k in Seg (len S02) or divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) )
reconsider S = T . i as Division of ['a,c'] ;
consider S1 being Division of ['a,b'], S2 being Division of ['b,c'] such that
A102: S1 = T1 . i and
A103: S2 = T2 . i and
A104: T . i = S1 ^ S2 by A82;
assume A105: k in Seg (len S02) ; :: thesis: divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)
then A106: k in dom S2 by A101, A103, FINSEQ_1:def 3;
then A107: (len S1) + k in dom S by A104, FINSEQ_1:28;
A108: divset ((T2 . i),k) = [.(lower_bound (divset ((T2 . i),k))),(upper_bound (divset ((T2 . i),k))).] by INTEGRA1:4;
A109: divset ((T . i),((len S1) + k)) = [.(lower_bound (divset ((T . i),((len S1) + k)))),(upper_bound (divset ((T . i),((len S1) + k)))).] by INTEGRA1:4;
A110: now :: thesis: ( k <> 1 implies divset ((T . i),((len S1) + k)) = divset ((T2 . i),k) )
( k <= len S2 & k - 1 <= k - 0 ) by A101, A105, A103, FINSEQ_1:1, XREAL_1:10;
then A111: k - 1 <= len S2 by XXREAL_0:2;
assume A112: k <> 1 ; :: thesis: divset ((T . i),((len S1) + k)) = divset ((T2 . i),k)
A113: 1 <= k by A105, FINSEQ_1:1;
then A114: 1 < k by A112, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
then A115: 2 - 1 <= k - 1 by XREAL_1:9;
k - 1 is Element of NAT by A114, NAT_1:20;
then k - 1 in Seg (len S2) by A111, A115, FINSEQ_1:1;
then A116: k - 1 in dom S2 by FINSEQ_1:def 3;
A117: 1 + 0 < k + (len S1) by A113, XREAL_1:8;
hence divset ((T . i),((len S1) + k)) = [.(S . (((len S1) + k) - 1)),(upper_bound (divset ((T . i),((len S1) + k)))).] by A107, A109, INTEGRA1:def 4
.= [.(S . (((len S1) + k) - 1)),(S . ((len S1) + k)).] by A107, A117, INTEGRA1:def 4
.= [.(S . ((len S1) + (k - 1))),(S2 . k).] by A104, A106, FINSEQ_1:def 7
.= [.(S2 . (k - 1)),(S2 . k).] by A104, A116, FINSEQ_1:def 7
.= [.(lower_bound (divset ((T2 . i),k))),(S2 . k).] by A103, A106, A112, INTEGRA1:def 4
.= divset ((T2 . i),k) by A103, A106, A108, A112, INTEGRA1:def 4 ;
:: thesis: verum
end;
now :: thesis: ( k = 1 implies divset ((T . i),((len S1) + k)) = divset ((T2 . i),k) )
len S1 in Seg (len S1) by FINSEQ_1:3;
then A118: len S1 in dom S1 by FINSEQ_1:def 3;
assume A119: k = 1 ; :: thesis: divset ((T . i),((len S1) + k)) = divset ((T2 . i),k)
len S1 <> 0 ;
then A120: (len S1) + k <> 1 by A119;
hence divset ((T . i),((len S1) + k)) = [.(S . (((len S1) + k) - 1)),(upper_bound (divset ((T . i),((len S1) + k)))).] by A107, A109, INTEGRA1:def 4
.= [.(S1 . (len S1)),(upper_bound (divset ((T . i),((len S1) + k)))).] by A104, A119, A118, FINSEQ_1:def 7
.= [.(upper_bound ['a,b']),(upper_bound (divset ((T . i),((len S1) + k)))).] by INTEGRA1:def 2
.= [.(lower_bound ['b,c']),(S . ((len S1) + k)).] by A14, A107, A120, INTEGRA1:def 4
.= [.(lower_bound ['b,c']),(S2 . k).] by A104, A106, FINSEQ_1:def 7
.= [.(lower_bound (divset ((T2 . i),k))),(S2 . 1).] by A103, A106, A119, INTEGRA1:def 4
.= divset ((T2 . i),k) by A103, A106, A108, A119, INTEGRA1:def 4 ;
:: thesis: verum
end;
hence divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) by A100, A102, A110; :: thesis: verum
end;
A121: for i, k being Element of NAT
for S0 being Division of ['b,c'] st S0 = T2 . i & k in Seg (len S0) holds
divset ((T2 . i),k) c= ['b,c']
proof
let i, k be Element of NAT ; :: thesis: for S0 being Division of ['b,c'] st S0 = T2 . i & k in Seg (len S0) holds
divset ((T2 . i),k) c= ['b,c']
let S0 be Division of ['b,c']; :: thesis: ( S0 = T2 . i & k in Seg (len S0) implies divset ((T2 . i),k) c= ['b,c'] )
assume that
A122: S0 = T2 . i and
A123: k in Seg (len S0) ; :: thesis: divset ((T2 . i),k) c= ['b,c']
k in dom S0 by A123, FINSEQ_1:def 3;
hence divset ((T2 . i),k) c= ['b,c'] by A122, INTEGRA1:8; :: thesis: verum
end;
A124: for i, k being Element of NAT
for S0 being Division of ['a,b'] st S0 = T1 . i & k in Seg (len S0) holds
divset ((T1 . i),k) c= ['a,b']
proof
let i, k be Element of NAT ; :: thesis: for S0 being Division of ['a,b'] st S0 = T1 . i & k in Seg (len S0) holds
divset ((T1 . i),k) c= ['a,b']
let S0 be Division of ['a,b']; :: thesis: ( S0 = T1 . i & k in Seg (len S0) implies divset ((T1 . i),k) c= ['a,b'] )
assume that
A125: S0 = T1 . i and
A126: k in Seg (len S0) ; :: thesis: divset ((T1 . i),k) c= ['a,b']
k in dom S0 by A126, FINSEQ_1:def 3;
hence divset ((T1 . i),k) c= ['a,b'] by A125, INTEGRA1:8; :: thesis: verum
end;
A127: for i being Element of NAT holds upper_volume ((f || ['a,c']),(T . i)) = (upper_volume ((f || ['a,b']),(T1 . i))) ^ (upper_volume ((f || ['b,c']),(T2 . i)))
proof
let i be Element of NAT ; :: thesis: upper_volume ((f || ['a,c']),(T . i)) = (upper_volume ((f || ['a,b']),(T1 . i))) ^ (upper_volume ((f || ['b,c']),(T2 . i)))
reconsider F = upper_volume ((f || ['a,c']),(T . i)) as FinSequence of REAL ;
reconsider F1 = upper_volume ((f || ['a,b']),(T1 . i)) as FinSequence of REAL ;
reconsider F2 = upper_volume ((f || ['b,c']),(T2 . i)) as FinSequence of REAL ;
reconsider S = T . i as Division of ['a,c'] ;
consider S1 being Division of ['a,b'], S2 being Division of ['b,c'] such that
A128: S1 = T1 . i and
A129: S2 = T2 . i and
A130: T . i = S1 ^ S2 by A82;
A131: len F = len S by INTEGRA1:def 6
.= (len S1) + (len S2) by A130, FINSEQ_1:22
.= (len F1) + (len S2) by A128, INTEGRA1:def 6
.= (len F1) + (len F2) by A129, INTEGRA1:def 6 ;
A132: now :: thesis: for k being Nat st k in dom F2 holds
F . ((len F1) + k) = F2 . k
let k be Nat; :: thesis: ( k in dom F2 implies F . ((len F1) + k) = F2 . k )
assume A133: k in dom F2 ; :: thesis: F . ((len F1) + k) = F2 . k
then A134: k in Seg (len F2) by FINSEQ_1:def 3;
then 1 <= k by FINSEQ_1:1;
then A135: 1 + (len F1) <= k + (len F1) by XREAL_1:6;
A136: k <= len F2 by A134, FINSEQ_1:1;
1 <= 1 + (len F1) by NAT_1:11;
then 1 <= k + (len F1) by A135, XXREAL_0:2;
then k + (len F1) in Seg (len F) by A136, A131, XREAL_1:6, FINSEQ_1:1;
then (len F1) + k in Seg (len S) by INTEGRA1:def 6;
then (len F1) + k in dom S by FINSEQ_1:def 3;
then A137: F . ((len F1) + k) = (upper_bound (rng ((f || ['a,c']) | (divset ((T . i),((len F1) + k)))))) * (vol (divset ((T . i),((len F1) + k)))) by INTEGRA1:def 6;
k in Seg (len F2) by A133, FINSEQ_1:def 3;
then A138: k in Seg (len S2) by A129, INTEGRA1:def 6;
then A139: k in dom S2 by FINSEQ_1:def 3;
len F1 = len S1 by A128, INTEGRA1:def 6;
then A140: divset ((T . i),((len F1) + k)) = divset ((T2 . i),k) by A99, A128, A129, A138;
then A141: divset ((T . i),((len F1) + k)) c= ['b,c'] by A121, A129, A138;
then divset ((T . i),((len F1) + k)) c= ['a,c'] by A12;
then F . ((len F1) + k) = (upper_bound (rng ((f || ['b,c']) | (divset ((T2 . i),k))))) * (vol (divset ((T2 . i),k))) by A137, A140, A141, INTEGRA6:3;
hence F . ((len F1) + k) = F2 . k by A129, A139, INTEGRA1:def 6; :: thesis: verum
end;
A142: now :: thesis: for k being Nat st k in dom F1 holds
F . k = F1 . k
let k be Nat; :: thesis: ( k in dom F1 implies F . k = F1 . k )
assume k in dom F1 ; :: thesis: F . k = F1 . k
then A143: k in Seg (len F1) by FINSEQ_1:def 3;
then A144: k in Seg (len S1) by A128, INTEGRA1:def 6;
then A145: k in dom S1 by FINSEQ_1:def 3;
Seg (len F1) c= Seg (len F) by A131, NAT_1:11, FINSEQ_1:5;
then k in Seg (len F) by A143;
then k in Seg (len S) by INTEGRA1:def 6;
then k in dom S by FINSEQ_1:def 3;
then A146: F . k = (upper_bound (rng ((f || ['a,c']) | (divset ((T . i),k))))) * (vol (divset ((T . i),k))) by INTEGRA1:def 6;
A147: divset ((T . i),k) = divset ((T1 . i),k) by A83, A128, A144;
then A148: divset ((T . i),k) c= ['a,b'] by A124, A128, A144;
then divset ((T . i),k) c= ['a,c'] by A12;
then F . k = (upper_bound (rng ((f || ['a,b']) | (divset ((T1 . i),k))))) * (vol (divset ((T1 . i),k))) by A146, A147, A148, INTEGRA6:3;
hence F . k = F1 . k by A128, A145, INTEGRA1:def 6; :: thesis: verum
end;
dom F = Seg ((len F1) + (len F2)) by A131, FINSEQ_1:def 3;
hence upper_volume ((f || ['a,c']),(T . i)) = (upper_volume ((f || ['a,b']),(T1 . i))) ^ (upper_volume ((f || ['b,c']),(T2 . i))) by A142, A132, FINSEQ_1:def 7; :: thesis: verum
end;
A149: for i being Element of NAT holds Sum (upper_volume ((f || ['a,c']),(T . i))) = (Sum (upper_volume ((f || ['a,b']),(T1 . i)))) + (Sum (upper_volume ((f || ['b,c']),(T2 . i))))
proof
let i be Element of NAT ; :: thesis: Sum (upper_volume ((f || ['a,c']),(T . i))) = (Sum (upper_volume ((f || ['a,b']),(T1 . i)))) + (Sum (upper_volume ((f || ['b,c']),(T2 . i))))
upper_volume ((f || ['a,c']),(T . i)) = (upper_volume ((f || ['a,b']),(T1 . i))) ^ (upper_volume ((f || ['b,c']),(T2 . i))) by A127;
hence Sum (upper_volume ((f || ['a,c']),(T . i))) = (Sum (upper_volume ((f || ['a,b']),(T1 . i)))) + (Sum (upper_volume ((f || ['b,c']),(T2 . i)))) by RVSUM_1:75; :: thesis: verum
end;
now :: thesis: for i being Nat holds (upper_sum ((f || ['a,c']),T)) . i = ((upper_sum ((f || ['a,b']),T1)) . i) + ((upper_sum ((f || ['b,c']),T2)) . i)
let i be Nat; :: thesis: (upper_sum ((f || ['a,c']),T)) . i = ((upper_sum ((f || ['a,b']),T1)) . i) + ((upper_sum ((f || ['b,c']),T2)) . i)
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
thus (upper_sum ((f || ['a,c']),T)) . i = upper_sum ((f || ['a,c']),(T . ii)) by INTEGRA2:def 2
.= Sum (upper_volume ((f || ['a,c']),(T . ii))) by INTEGRA1:def 8
.= (Sum (upper_volume ((f || ['a,b']),(T1 . i)))) + (Sum (upper_volume ((f || ['b,c']),(T2 . i)))) by A149
.= (upper_sum ((f || ['a,b']),(T1 . ii))) + (Sum (upper_volume ((f || ['b,c']),(T2 . ii)))) by INTEGRA1:def 8
.= (upper_sum ((f || ['a,b']),(T1 . ii))) + (upper_sum ((f || ['b,c']),(T2 . ii))) by INTEGRA1:def 8
.= ((upper_sum ((f || ['a,b']),T1)) . i) + (upper_sum ((f || ['b,c']),(T2 . ii))) by INTEGRA2:def 2
.= ((upper_sum ((f || ['a,b']),T1)) . i) + ((upper_sum ((f || ['b,c']),T2)) . i) by INTEGRA2:def 2 ; :: thesis: verum
end;
then A150: upper_sum ((f || ['a,c']),T) = (upper_sum ((f || ['a,b']),T1)) + (upper_sum ((f || ['b,c']),T2)) by SEQ_1:7;
A151: now :: thesis: for e being Real st 0 < e holds
ex m being Nat st
for n being Nat st m <= n holds
|.(((delta S2) . n) - 0).| < e
let e be Real; :: thesis: ( 0 < e implies ex m being Nat st
for n being Nat st m <= n holds
|.(((delta S2) . n) - 0).| < e )
assume 0 < e ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
|.(((delta S2) . n) - 0).| < e
then consider m being Nat such that
A152: for n being Nat st m <= n holds
|.(((delta PS2) . n) - 0).| < e by A15, SEQ_2:def 7;
take m = m; :: thesis: for n being Nat st m <= n holds
|.(((delta S2) . n) - 0).| < e
hereby :: thesis: verum
let n be Nat; :: thesis: ( m <= n implies |.(((delta S2) . n) - 0).| < e )
A153: n <= n + 2 by NAT_1:11;
assume m <= n ; :: thesis: |.(((delta S2) . n) - 0).| < e
then m <= n + 2 by A153, XXREAL_0:2;
then |.(((delta PS2) . (n + 2)) - 0).| < e by A152;
then A154: |.((delta (PS2 . (n + 2))) - 0).| < e by INTEGRA3:def 2;
n in NAT by ORDINAL1:def 12;
then ex k being Element of NAT ex e1 being Division of ['b,c'] st
( k = n & e1 = S2 . n & e1 = PS2 . (k + 2) ) by A22;
hence |.(((delta S2) . n) - 0).| < e by A154, INTEGRA3:def 2; :: thesis: verum
end;
end;
set XBC = chi (['b,c'],['b,c']);
A155: now :: thesis: for e being Real st e > 0 holds
ex m being Nat st
for nn being Nat st m <= nn holds
|.(((delta T2) . nn) - 0).| < e
let e be Real; :: thesis: ( e > 0 implies ex m being Nat st
for nn being Nat st m <= nn holds
|.(((delta T2) . nn) - 0).| < e )
assume A156: e > 0 ; :: thesis: ex m being Nat st
for nn being Nat st m <= nn holds
|.(((delta T2) . nn) - 0).| < e
then consider m being Nat such that
A157: for n being Nat st m <= n holds
|.(((delta S2) . n) - 0).| < e / 2 by A151, XREAL_1:215;
take m = m; :: thesis: for nn being Nat st m <= nn holds
|.(((delta T2) . nn) - 0).| < e
A158: e / 2 < e by A156, XREAL_1:216;
let nn be Nat; :: thesis: ( m <= nn implies |.(((delta T2) . nn) - 0).| < e )
assume A159: m <= nn ; :: thesis: |.(((delta T2) . nn) - 0).| < e
reconsider n = nn as Element of NAT by ORDINAL1:def 12;
|.(((delta S2) . n) - 0).| < e / 2 by A157, A159;
then ( 0 <= delta (S2 . n) & |.(delta (S2 . n)).| < e / 2 ) by INTEGRA3:9, INTEGRA3:def 2;
then delta (S2 . n) < e / 2 by ABSVALUE:def 1;
then A160: max (rng (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n)))) < e / 2 by INTEGRA3:def 1;
A161: for y being Real st y in rng (upper_volume ((chi (['b,c'],['b,c'])),(T2 . n))) holds
y < e
proof
reconsider D = T2 . n as Division of ['b,c'] ;
let y be Real; :: thesis: ( y in rng (upper_volume ((chi (['b,c'],['b,c'])),(T2 . n))) implies y < e )
assume y in rng (upper_volume ((chi (['b,c'],['b,c'])),(T2 . n))) ; :: thesis: y < e
then consider x being object such that
A162: x in dom (upper_volume ((chi (['b,c'],['b,c'])),(T2 . n))) and
A163: y = (upper_volume ((chi (['b,c'],['b,c'])),(T2 . n))) . x by FUNCT_1:def 3;
reconsider i = x as Element of NAT by A162;
A164: x in Seg (len (upper_volume ((chi (['b,c'],['b,c'])),(T2 . n)))) by A162, FINSEQ_1:def 3;
consider E1 being Division of ['b,c'] such that
A165: E1 = S2 . n and
A166: 2 <= len E1 by A23;
set i1 = i + 1;
consider E being Division of ['b,c'] such that
A167: E = S2 . n and
A168: T2 . n = E /^ 1 by A31;
A169: 1 <= len E1 by A166, XXREAL_0:2;
then A170: len D = (len E) - 1 by A167, A168, A165, RFINSEQ:def 1;
A171: len (upper_volume ((chi (['b,c'],['b,c'])),(T2 . n))) = len D by INTEGRA1:def 6;
then A172: dom (upper_volume ((chi (['b,c'],['b,c'])),(T2 . n))) = dom D by FINSEQ_3:29;
A173: now :: thesis: ( i = 1 implies y < e )
len (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) = len E by A167, INTEGRA1:def 6;
then 2 in Seg (len (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n)))) by A167, A165, A166, FINSEQ_1:1;
then 2 in dom (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) by FINSEQ_1:def 3;
then (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) . 2 in rng (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) by FUNCT_1:def 3;
then (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) . 2 <= max (rng (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n)))) by XXREAL_2:def 8;
then A174: (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) . 2 < e / 2 by A160, XXREAL_0:2;
assume A175: i = 1 ; :: thesis: y < e
then A176: 1 in dom D by A164, A171, FINSEQ_1:def 3;
len (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) = (len D) + 1 by A167, A170, INTEGRA1:def 6;
then len (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) = (len (upper_volume ((chi (['b,c'],['b,c'])),(T2 . n)))) + 1 by INTEGRA1:def 6;
then 1 in Seg (len (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n)))) by A164, A175, FINSEQ_2:8;
then 1 in dom (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) by FINSEQ_1:def 3;
then (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) . 1 in rng (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) by FUNCT_1:def 3;
then (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) . 1 <= max (rng (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n)))) by XXREAL_2:def 8;
then A177: (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) . 1 < e / 2 by A160, XXREAL_0:2;
A178: 2 in dom E by A167, A165, A166, FINSEQ_3:25;
1 in Seg (len E) by A167, A165, A169, FINSEQ_1:1;
then A179: 1 in dom E by FINSEQ_1:def 3;
divset ((S2 . n),1) = [.(lower_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),1))).] by INTEGRA1:4;
then A180: divset ((S2 . n),1) = [.(lower_bound ['b,c']),(upper_bound (divset ((S2 . n),1))).] by A167, A179, INTEGRA1:def 4;
then A181: [.(lower_bound ['b,c']),(upper_bound (divset ((S2 . n),1))).] = [.(lower_bound [.(lower_bound ['b,c']),(upper_bound (divset ((S2 . n),1))).]),(upper_bound [.(lower_bound ['b,c']),(upper_bound (divset ((S2 . n),1))).]).] by INTEGRA1:4;
A182: divset ((T2 . n),i) = [.(lower_bound (divset ((T2 . n),1))),(upper_bound (divset ((T2 . n),1))).] by A175, INTEGRA1:4
.= [.(lower_bound ['b,c']),(upper_bound (divset ((T2 . n),1))).] by A176, INTEGRA1:def 4
.= [.(lower_bound ['b,c']),(D . 1).] by A176, INTEGRA1:def 4
.= [.(lower_bound ['b,c']),(E . (1 + 1)).] by A167, A168, A165, A169, A176, RFINSEQ:def 1
.= [.(lower_bound ['b,c']),(upper_bound (divset ((S2 . n),2))).] by A167, A178, INTEGRA1:def 4 ;
then [.(lower_bound ['b,c']),(upper_bound (divset ((S2 . n),2))).] = [.(lower_bound [.(lower_bound ['b,c']),(upper_bound (divset ((S2 . n),2))).]),(upper_bound [.(lower_bound ['b,c']),(upper_bound (divset ((S2 . n),2))).]).] by INTEGRA1:4;
then A183: ( lower_bound ['b,c'] = lower_bound [.(lower_bound ['b,c']),(upper_bound (divset ((S2 . n),2))).] & upper_bound (divset ((S2 . n),2)) = upper_bound [.(lower_bound ['b,c']),(upper_bound (divset ((S2 . n),2))).] ) by A182, INTEGRA1:5;
y = vol (divset ((T2 . n),1)) by A162, A163, A172, A175, INTEGRA1:20;
then y = (upper_bound (divset ((T2 . n),1))) - (lower_bound (divset ((T2 . n),1))) by INTEGRA1:def 5;
then y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + ((upper_bound [.(lower_bound ['b,c']),(upper_bound (divset ((S2 . n),1))).]) - (lower_bound ['b,c'])) by A175, A182, A183, A180;
then y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + ((upper_bound (divset ((S2 . n),1))) - (lower_bound (divset ((S2 . n),1)))) by A180, A181, INTEGRA1:5;
then A184: y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + (vol (divset ((S2 . n),1))) by INTEGRA1:def 5;
divset ((S2 . n),2) = [.(lower_bound (divset ((S2 . n),2))),(upper_bound (divset ((S2 . n),2))).] by INTEGRA1:4;
then divset ((S2 . n),2) = [.(E . (2 - 1)),(upper_bound (divset ((S2 . n),2))).] by A167, A178, INTEGRA1:def 4;
then A185: divset ((S2 . n),2) = [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).] by A167, A179, INTEGRA1:def 4;
then [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).] = [.(lower_bound [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).]),(upper_bound [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).]).] by INTEGRA1:4;
then y = ((upper_bound (divset ((S2 . n),2))) - (lower_bound (divset ((S2 . n),2)))) + (vol (divset ((S2 . n),1))) by A185, A184, INTEGRA1:5;
then y = (vol (divset ((S2 . n),2))) + (vol (divset ((S2 . n),1))) by INTEGRA1:def 5;
then y = ((upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) . 2) + (vol (divset ((S2 . n),1))) by A167, A178, INTEGRA1:20;
then y = ((upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) . 2) + ((upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) . 1) by A167, A179, INTEGRA1:20;
then y < (e / 2) + (e / 2) by A174, A177, XREAL_1:8;
hence y < e ; :: thesis: verum
end;
A186: y = (upper_bound (rng ((chi (['b,c'],['b,c'])) | (divset ((T2 . n),i))))) * (vol (divset ((T2 . n),i))) by A162, A163, A172, INTEGRA1:def 6;
now :: thesis: ( i <> 1 implies y < e )
len (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) = (len D) + 1 by A167, A170, INTEGRA1:def 6;
then len (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) = (len (upper_volume ((chi (['b,c'],['b,c'])),(T2 . n)))) + 1 by INTEGRA1:def 6;
then A187: i + 1 in Seg (len (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n)))) by A164, FINSEQ_1:60;
then A188: i + 1 in dom (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) by FINSEQ_1:def 3;
A189: i + 1 in dom (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) by A187, FINSEQ_1:def 3;
A190: i in dom D by A164, A171, FINSEQ_1:def 3;
Seg ((len D) + 1) = Seg (len E) by A170;
then i + 1 in Seg (len E) by A164, A171, FINSEQ_1:60;
then A191: i + 1 in dom E by FINSEQ_1:def 3;
len (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) = len E by A167, INTEGRA1:def 6;
then A192: dom (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) = dom E by FINSEQ_3:29;
assume A193: i <> 1 ; :: thesis: y < e
i in Seg (len D) by A162, A171, FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:1;
then A194: 1 < i by A193, XXREAL_0:1;
then A195: i - 1 in Seg (len D) by A164, A171, FINSEQ_3:12;
then A196: i - 1 in dom D by FINSEQ_1:def 3;
reconsider i9 = i - 1 as Element of NAT by A195;
1 + 1 < i + 1 by A194, XREAL_1:8;
then A197: i + 1 <> 1 ;
divset ((T2 . n),i) = [.(lower_bound (divset ((T2 . n),i))),(upper_bound (divset ((T2 . n),i))).] by INTEGRA1:4
.= [.(D . (i - 1)),(upper_bound (divset ((T2 . n),i))).] by A193, A190, INTEGRA1:def 4
.= [.(D . (i - 1)),(D . i).] by A193, A190, INTEGRA1:def 4
.= [.(E . (i9 + 1)),(D . i).] by A167, A168, A165, A169, A196, RFINSEQ:def 1
.= [.(E . ((i - 1) + 1)),(E . (i + 1)).] by A167, A168, A165, A169, A190, RFINSEQ:def 1
.= [.(E . ((i + 1) - 1)),(upper_bound (divset ((S2 . n),(i + 1)))).] by A167, A197, A191, INTEGRA1:def 4
.= [.(lower_bound (divset ((S2 . n),(i + 1)))),(upper_bound (divset ((S2 . n),(i + 1)))).] by A167, A197, A191, INTEGRA1:def 4
.= divset ((S2 . n),(i + 1)) by INTEGRA1:4 ;
then y = (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) . (i + 1) by A186, A167, A188, A192, INTEGRA1:def 6;
then y in rng (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n))) by A189, FUNCT_1:def 3;
then y <= max (rng (upper_volume ((chi (['b,c'],['b,c'])),(S2 . n)))) by XXREAL_2:def 8;
then y < e / 2 by A160, XXREAL_0:2;
hence y < e by A158, XXREAL_0:2; :: thesis: verum
end;
hence y < e by A173; :: thesis: verum
end;
max (rng (upper_volume ((chi (['b,c'],['b,c'])),(T2 . n)))) in rng (upper_volume ((chi (['b,c'],['b,c'])),(T2 . n))) by XXREAL_2:def 8;
then max (rng (upper_volume ((chi (['b,c'],['b,c'])),(T2 . n)))) < e by A161;
then ( 0 <= delta (T2 . n) & delta (T2 . n) < e ) by INTEGRA3:9, INTEGRA3:def 1;
then |.(delta (T2 . n)).| < e by ABSVALUE:def 1;
hence |.(((delta T2) . nn) - 0).| < e by INTEGRA3:def 2; :: thesis: verum
end;
then A198: delta T2 is convergent by SEQ_2:def 6;
then A199: lim (delta T2) = 0 by A155, SEQ_2:def 7;
(f || ['b,c']) | ['b,c'] is bounded by A4;
then A200: ( upper_sum ((f || ['b,c']),T2) is convergent & lim (upper_sum ((f || ['b,c']),T2)) = upper_integral (f || ['b,c']) ) by A13, A198, A199, INTEGRA4:9;
set XAB = chi (['a,b'],['a,b']);
set XAC = chi (['a,c'],['a,c']);
A201: now :: thesis: for e being Real st 0 < e holds
ex n being Nat st
for mm being Nat st n <= mm holds
|.(((delta T) . mm) - 0).| < e
let e be Real; :: thesis: ( 0 < e implies ex n being Nat st
for mm being Nat st n <= mm holds
|.(((delta T) . mm) - 0).| < e )
assume A202: 0 < e ; :: thesis: ex n being Nat st
for mm being Nat st n <= mm holds
|.(((delta T) . mm) - 0).| < e
then consider n1 being Nat such that
A203: for m being Nat st n1 <= m holds
|.(((delta T1) . m) - 0).| < e by A46, SEQ_2:def 7;
consider n2 being Nat such that
A204: for m being Nat st n2 <= m holds
|.(((delta T2) . m) - 0).| < e by A155, A202;
reconsider n = max (n1,n2) as Nat by TARSKI:1;
take n = n; :: thesis: for mm being Nat st n <= mm holds
|.(((delta T) . mm) - 0).| < e
let mm be Nat; :: thesis: ( n <= mm implies |.(((delta T) . mm) - 0).| < e )
assume A205: n <= mm ; :: thesis: |.(((delta T) . mm) - 0).| < e
reconsider m = mm as Element of NAT by ORDINAL1:def 12;
n2 <= n by XXREAL_0:25;
then n2 <= m by A205, XXREAL_0:2;
then |.(((delta T2) . m) - 0).| < e by A204;
then |.(delta (T2 . m)).| < e by INTEGRA3:def 2;
then delta (T2 . m) < e by INTEGRA3:9, ABSVALUE:def 1;
then A206: max (rng (upper_volume ((chi (['b,c'],['b,c'])),(T2 . m)))) < e by INTEGRA3:def 1;
n1 <= n by XXREAL_0:25;
then n1 <= m by A205, XXREAL_0:2;
then |.(((delta T1) . m) - 0).| < e by A203;
then |.(delta (T1 . m)).| < e by INTEGRA3:def 2;
then delta (T1 . m) < e by INTEGRA3:9, ABSVALUE:def 1;
then A207: max (rng (upper_volume ((chi (['a,b'],['a,b'])),(T1 . m)))) < e by INTEGRA3:def 1;
A208: for r being Real st r in rng (upper_volume ((chi (['a,c'],['a,c'])),(T . m))) holds
r < e
proof
reconsider Tm = T . m as Division of ['a,c'] ;
let y be Real; :: thesis: ( y in rng (upper_volume ((chi (['a,c'],['a,c'])),(T . m))) implies y < e )
assume y in rng (upper_volume ((chi (['a,c'],['a,c'])),(T . m))) ; :: thesis: y < e
then consider x being object such that
A209: x in dom (upper_volume ((chi (['a,c'],['a,c'])),(T . m))) and
A210: y = (upper_volume ((chi (['a,c'],['a,c'])),(T . m))) . x by FUNCT_1:def 3;
reconsider i = x as Element of NAT by A209;
A211: x in Seg (len (upper_volume ((chi (['a,c'],['a,c'])),(T . m)))) by A209, FINSEQ_1:def 3;
then A212: 1 <= i by FINSEQ_1:1;
A213: len (upper_volume ((chi (['a,c'],['a,c'])),(T . m))) = len Tm by INTEGRA1:def 6;
then A214: i <= len Tm by A211, FINSEQ_1:1;
dom (upper_volume ((chi (['a,c'],['a,c'])),(T . m))) = dom Tm by A213, FINSEQ_3:29;
then A215: y = (upper_bound (rng ((chi (['a,c'],['a,c'])) | (divset ((T . m),i))))) * (vol (divset ((T . m),i))) by A209, A210, INTEGRA1:def 6;
consider S1 being Division of ['a,b'], S2 being Division of ['b,c'] such that
A216: S1 = T1 . m and
A217: S2 = T2 . m and
A218: T . m = S1 ^ S2 by A82;
A219: len Tm = (len S1) + (len S2) by A218, FINSEQ_1:22;
per cases ( i <= len S1 or i > len S1 ) ;
suppose i <= len S1 ; :: thesis: y < e
then A220: i in Seg (len S1) by A212, FINSEQ_1:1;
then A221: i in dom S1 by FINSEQ_1:def 3;
len (upper_volume ((chi (['a,b'],['a,b'])),(T1 . m))) = len S1 by A216, INTEGRA1:def 6;
then A222: i in dom (upper_volume ((chi (['a,b'],['a,b'])),(T1 . m))) by A220, FINSEQ_1:def 3;
A223: divset ((T1 . m),i) = divset ((T . m),i) by A83, A216, A220;
A224: divset ((T1 . m),i) c= ['a,b'] by A124, A216, A220;
then divset ((T1 . m),i) c= ['a,c'] by A12;
then (chi (['a,b'],['a,b'])) | (divset ((T1 . m),i)) = (chi (['a,c'],['a,c'])) | (divset ((T . m),i)) by A223, A224, INTEGRA6:4;
then y = (upper_volume ((chi (['a,b'],['a,b'])),(T1 . m))) . i by A215, A216, A221, A223, INTEGRA1:def 6;
then y in rng (upper_volume ((chi (['a,b'],['a,b'])),(T1 . m))) by A222, FUNCT_1:def 3;
then y <= max (rng (upper_volume ((chi (['a,b'],['a,b'])),(T1 . m)))) by XXREAL_2:def 8;
hence y < e by A207, XXREAL_0:2; :: thesis: verum
end;
suppose i > len S1 ; :: thesis: y < e
then A225: (len S1) + 1 <= i by NAT_1:13;
then consider k being Nat such that
A226: ((len S1) + 1) + k = i by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
set i1 = 1 + k;
A227: i - (len S1) <= len S2 by A219, A214, XREAL_1:20;
1 + k = i - (len S1) by A226;
then 1 <= 1 + k by A225, XREAL_1:19;
then A228: 1 + k in Seg (len S2) by A226, A227, FINSEQ_1:1;
then A229: 1 + k in dom S2 by FINSEQ_1:def 3;
A230: divset ((T2 . m),(1 + k)) = divset ((T . m),((len S1) + (1 + k))) by A99, A216, A217, A228;
A231: divset ((T2 . m),(1 + k)) c= ['b,c'] by A121, A217, A228;
then divset ((T2 . m),(1 + k)) c= ['a,c'] by A12;
then y = (upper_bound (rng ((chi (['b,c'],['b,c'])) | (divset ((T2 . m),(1 + k)))))) * (vol (divset ((T2 . m),(1 + k)))) by A215, A226, A230, A231, INTEGRA6:4;
then A232: y = (upper_volume ((chi (['b,c'],['b,c'])),(T2 . m))) . (1 + k) by A217, A229, INTEGRA1:def 6;
len (upper_volume ((chi (['b,c'],['b,c'])),(T2 . m))) = len S2 by A217, INTEGRA1:def 6;
then 1 + k in dom (upper_volume ((chi (['b,c'],['b,c'])),(T2 . m))) by A228, FINSEQ_1:def 3;
then y in rng (upper_volume ((chi (['b,c'],['b,c'])),(T2 . m))) by A232, FUNCT_1:def 3;
then y <= max (rng (upper_volume ((chi (['b,c'],['b,c'])),(T2 . m)))) by XXREAL_2:def 8;
hence y < e by A206, XXREAL_0:2; :: thesis: verum
end;
end;
end;
max (rng (upper_volume ((chi (['a,c'],['a,c'])),(T . m)))) in rng (upper_volume ((chi (['a,c'],['a,c'])),(T . m))) by XXREAL_2:def 8;
then max (rng (upper_volume ((chi (['a,c'],['a,c'])),(T . m)))) < e by A208;
then delta (T . m) < e by INTEGRA3:def 1;
then |.(delta (T . m)).| < e by INTEGRA3:9, ABSVALUE:def 1;
hence |.(((delta T) . mm) - 0).| < e by INTEGRA3:def 2; :: thesis: verum
end;
then A233: delta T is convergent by SEQ_2:def 6;
then A234: lim (delta T) = 0 by A201, SEQ_2:def 7;
(f || ['a,c']) | ['a,c'] is bounded by A10, A3, A4, RFUNCT_1:87;
then A235: upper_integral (f || ['a,c']) = lim (upper_sum ((f || ['a,c']),T)) by A8, A233, A234, INTEGRA4:9;
A236: for i being Element of NAT holds lower_volume ((f || ['a,c']),(T . i)) = (lower_volume ((f || ['a,b']),(T1 . i))) ^ (lower_volume ((f || ['b,c']),(T2 . i)))
proof
let i be Element of NAT ; :: thesis: lower_volume ((f || ['a,c']),(T . i)) = (lower_volume ((f || ['a,b']),(T1 . i))) ^ (lower_volume ((f || ['b,c']),(T2 . i)))
reconsider F = lower_volume ((f || ['a,c']),(T . i)) as FinSequence of REAL ;
reconsider F1 = lower_volume ((f || ['a,b']),(T1 . i)) as FinSequence of REAL ;
reconsider F2 = lower_volume ((f || ['b,c']),(T2 . i)) as FinSequence of REAL ;
reconsider S = T . i as Division of ['a,c'] ;
consider S1 being Division of ['a,b'], S2 being Division of ['b,c'] such that
A237: S1 = T1 . i and
A238: S2 = T2 . i and
A239: T . i = S1 ^ S2 by A82;
A240: len F = len S by INTEGRA1:def 7
.= (len S1) + (len S2) by A239, FINSEQ_1:22
.= (len F1) + (len S2) by A237, INTEGRA1:def 7 ;
then A241: len F = (len F1) + (len F2) by A238, INTEGRA1:def 7;
A242: now :: thesis: for k being Nat st k in dom F2 holds
F . ((len F1) + k) = F2 . k
let k be Nat; :: thesis: ( k in dom F2 implies F . ((len F1) + k) = F2 . k )
assume k in dom F2 ; :: thesis: F . ((len F1) + k) = F2 . k
then A243: k in Seg (len F2) by FINSEQ_1:def 3;
then 1 <= k by FINSEQ_1:1;
then A244: 1 + (len F1) <= k + (len F1) by XREAL_1:6;
A245: k <= len F2 by A243, FINSEQ_1:1;
1 <= 1 + (len F1) by NAT_1:11;
then 1 <= k + (len F1) by A244, XXREAL_0:2;
then k + (len F1) in Seg (len F) by A245, A241, XREAL_1:6, FINSEQ_1:1;
then (len F1) + k in Seg (len S) by INTEGRA1:def 7;
then (len F1) + k in dom S by FINSEQ_1:def 3;
then A246: F . ((len F1) + k) = (lower_bound (rng ((f || ['a,c']) | (divset ((T . i),((len F1) + k)))))) * (vol (divset ((T . i),((len F1) + k)))) by INTEGRA1:def 7;
A247: k in Seg (len S2) by A238, A243, INTEGRA1:def 7;
then A248: k in dom S2 by FINSEQ_1:def 3;
len F1 = len S1 by A237, INTEGRA1:def 7;
then A249: divset ((T . i),((len F1) + k)) = divset ((T2 . i),k) by A99, A237, A238, A247;
A250: divset ((T2 . i),k) c= ['b,c'] by A121, A238, A247;
then divset ((T . i),((len F1) + k)) c= ['a,c'] by A12, A249;
then F . ((len F1) + k) = (lower_bound (rng ((f || ['b,c']) | (divset ((T2 . i),k))))) * (vol (divset ((T2 . i),k))) by A246, A249, A250, INTEGRA6:3;
hence F . ((len F1) + k) = F2 . k by A238, A248, INTEGRA1:def 7; :: thesis: verum
end;
A251: now :: thesis: for k being Nat st k in dom F1 holds
F . k = F1 . k
let k be Nat; :: thesis: ( k in dom F1 implies F . k = F1 . k )
len (lower_volume ((f || ['a,c']),(T . i))) = len S by INTEGRA1:def 7;
then A252: dom (lower_volume ((f || ['a,c']),(T . i))) = dom S by FINSEQ_3:29;
assume A253: k in dom F1 ; :: thesis: F . k = F1 . k
then k in Seg (len F1) by FINSEQ_1:def 3;
then A254: k in Seg (len S1) by A237, INTEGRA1:def 7;
then A255: k in dom S1 by FINSEQ_1:def 3;
dom F1 c= dom F by A240, NAT_1:11, FINSEQ_3:30;
then A256: F . k = (lower_bound (rng ((f || ['a,c']) | (divset ((T . i),k))))) * (vol (divset ((T . i),k))) by A253, A252, INTEGRA1:def 7;
A257: ( divset ((T . i),k) = divset ((T1 . i),k) & divset ((T1 . i),k) c= ['a,b'] ) by A124, A83, A237, A254;
then divset ((T . i),k) c= ['a,c'] by A12;
then F . k = (lower_bound (rng ((f || ['a,b']) | (divset ((T1 . i),k))))) * (vol (divset ((T1 . i),k))) by A256, A257, INTEGRA6:3;
hence F . k = F1 . k by A237, A255, INTEGRA1:def 7; :: thesis: verum
end;
dom F = Seg ((len F1) + (len F2)) by A241, FINSEQ_1:def 3;
hence lower_volume ((f || ['a,c']),(T . i)) = (lower_volume ((f || ['a,b']),(T1 . i))) ^ (lower_volume ((f || ['b,c']),(T2 . i))) by A251, A242, FINSEQ_1:def 7; :: thesis: verum
end;
A258: for i being Element of NAT holds Sum (lower_volume ((f || ['a,c']),(T . i))) = (Sum (lower_volume ((f || ['a,b']),(T1 . i)))) + (Sum (lower_volume ((f || ['b,c']),(T2 . i))))
proof
let i be Element of NAT ; :: thesis: Sum (lower_volume ((f || ['a,c']),(T . i))) = (Sum (lower_volume ((f || ['a,b']),(T1 . i)))) + (Sum (lower_volume ((f || ['b,c']),(T2 . i))))
lower_volume ((f || ['a,c']),(T . i)) = (lower_volume ((f || ['a,b']),(T1 . i))) ^ (lower_volume ((f || ['b,c']),(T2 . i))) by A236;
hence Sum (lower_volume ((f || ['a,c']),(T . i))) = (Sum (lower_volume ((f || ['a,b']),(T1 . i)))) + (Sum (lower_volume ((f || ['b,c']),(T2 . i)))) by RVSUM_1:75; :: thesis: verum
end;
now :: thesis: for i being Nat holds (lower_sum ((f || ['a,c']),T)) . i = ((lower_sum ((f || ['a,b']),T1)) . i) + ((lower_sum ((f || ['b,c']),T2)) . i)
let i be Nat; :: thesis: (lower_sum ((f || ['a,c']),T)) . i = ((lower_sum ((f || ['a,b']),T1)) . i) + ((lower_sum ((f || ['b,c']),T2)) . i)
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
thus (lower_sum ((f || ['a,c']),T)) . i = lower_sum ((f || ['a,c']),(T . ii)) by INTEGRA2:def 3
.= Sum (lower_volume ((f || ['a,c']),(T . ii))) by INTEGRA1:def 9
.= (Sum (lower_volume ((f || ['a,b']),(T1 . i)))) + (Sum (lower_volume ((f || ['b,c']),(T2 . i)))) by A258
.= (lower_sum ((f || ['a,b']),(T1 . ii))) + (Sum (lower_volume ((f || ['b,c']),(T2 . ii)))) by INTEGRA1:def 9
.= (lower_sum ((f || ['a,b']),(T1 . ii))) + (lower_sum ((f || ['b,c']),(T2 . ii))) by INTEGRA1:def 9
.= ((lower_sum ((f || ['a,b']),T1)) . i) + (lower_sum ((f || ['b,c']),(T2 . ii))) by INTEGRA2:def 3
.= ((lower_sum ((f || ['a,b']),T1)) . i) + ((lower_sum ((f || ['b,c']),T2)) . i) by INTEGRA2:def 3 ; :: thesis: verum
end;
then A259: lower_sum ((f || ['a,c']),T) = (lower_sum ((f || ['a,b']),T1)) + (lower_sum ((f || ['b,c']),T2)) by SEQ_1:7;
A260: (f || ['a,b']) | ['a,b'] is bounded by A3;
then ( upper_sum ((f || ['a,b']),T1) is convergent & lim (upper_sum ((f || ['a,b']),T1)) = upper_integral (f || ['a,b']) ) by A13, A46, INTEGRA4:9;
then A261: (upper_integral (f || ['a,b'])) + (upper_integral (f || ['b,c'])) = upper_integral (f || ['a,c']) by A150, A200, A235, SEQ_2:6;
A262: ( lower_sum ((f || ['a,b']),T1) is convergent & lim (lower_sum ((f || ['a,b']),T1)) = lower_integral (f || ['a,b']) ) by A13, A260, A46, INTEGRA4:8;
(f || ['a,c']) | ['a,c'] is bounded by A10, A3, A4, RFUNCT_1:87;
then A263: lower_integral (f || ['a,c']) = lim (lower_sum ((f || ['a,c']),T)) by A8, A233, A234, INTEGRA4:8;
(f || ['b,c']) | ['b,c'] is bounded by A4;
then ( lower_sum ((f || ['b,c']),T2) is convergent & lim (lower_sum ((f || ['b,c']),T2)) = lower_integral (f || ['b,c']) ) by A13, A198, A199, INTEGRA4:8;
then A264: (lower_integral (f || ['a,b'])) + (lower_integral (f || ['b,c'])) = lower_integral (f || ['a,c']) by A259, A262, A263, SEQ_2:6;
A265: ( f || ['a,b'] is integrable & f || ['b,c'] is integrable ) by A5, A6, INTEGRA5:def 1;
then ( f || ['a,b'] is upper_integrable & f || ['a,b'] is lower_integrable & upper_integral (f || ['a,b']) = lower_integral (f || ['a,b']) ) by INTEGRA1:def 16;
then upper_integral (f || ['a,c']) = lower_integral (f || ['a,c']) by A264, A261, A265, INTEGRA1:def 16;
hence f is_integrable_on ['a,c'] by A11, INTEGRA1:def 16, INTEGRA5:def 1; :: thesis: verum