let a, b, c be Real; :: thesis: for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & c in ['a,b'] & b <> c holds
( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )

let f be PartFunc of REAL,REAL; :: thesis: ( a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & c in ['a,b'] & b <> c implies ( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) )
assume that
A1: a <= b and
A2: ['a,b'] c= dom f and
A3: f is_integrable_on ['a,b'] and
A4: f | ['a,b'] is bounded and
A5: c in ['a,b'] and
A6: b <> c ; :: thesis: ( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )
A7: ['a,b'] = [.a,b.] by ;
then A8: c <= b by ;
then A9: ['c,b'] = [.c,b.] by INTEGRA5:def 3;
then A10: [.c,b.] = [.(),().] by INTEGRA1:4;
then A11: upper_bound ['c,b'] = b by ;
set FAB = f || ['a,b'];
set FAC = f || ['a,c'];
set FCB = f || ['c,b'];
A12: f || ['a,b'] is Function of ['a,b'],REAL by ;
A13: a <= c by ;
then A14: ['a,c'] = [.a,c.] by INTEGRA5:def 3;
then A15: [.a,c.] = [.(),().] by INTEGRA1:4;
then A16: lower_bound ['a,c'] = a by ;
A17: ['c,b'] c= ['a,b'] by ;
then f | ['c,b'] is bounded by ;
then A18: (f || ['c,b']) | ['c,b'] is bounded ;
A19: lower_bound ['c,b'] = c by ;
ex PS2 being DivSequence of ['c,b'] st
( delta PS2 is convergent & lim (delta PS2) = 0 & ex K being Element of NAT st
for i being Element of NAT st K <= i holds
ex S2i being Division of ['c,b'] st
( S2i = PS2 . i & 2 <= len S2i ) )
proof
c < b by ;
then vol ['c,b'] > 0 by ;
then consider T being DivSequence of ['c,b'] such that
A20: ( delta T is convergent & lim () = 0 ) and
A21: for n being Element of NAT ex Tn being Division of ['c,b'] st
( Tn divide_into_equal n + 1 & T . n = Tn ) by Th16;
take T ; :: thesis: ( delta T is convergent & lim () = 0 & ex K being Element of NAT st
for i being Element of NAT st K <= i holds
ex S2i being Division of ['c,b'] st
( S2i = T . i & 2 <= len S2i ) )

now :: thesis: for i being Element of NAT st 2 <= i holds
ex Tn being Division of ['c,b'] st
( Tn = T . i & 2 <= len Tn )
let i be Element of NAT ; :: thesis: ( 2 <= i implies ex Tn being Division of ['c,b'] st
( Tn = T . i & 2 <= len Tn ) )

assume A22: 2 <= i ; :: thesis: ex Tn being Division of ['c,b'] st
( Tn = T . i & 2 <= len Tn )

consider Tn being Division of ['c,b'] such that
A23: Tn divide_into_equal i + 1 and
A24: T . i = Tn by A21;
reconsider Tn = Tn as Division of ['c,b'] ;
take Tn = Tn; :: thesis: ( Tn = T . i & 2 <= len Tn )
thus Tn = T . i by A24; :: thesis: 2 <= len Tn
len Tn = i + 1 by ;
then i <= len Tn by NAT_1:11;
hence 2 <= len Tn by ; :: thesis: verum
end;
hence ( delta T is convergent & lim () = 0 & ex K being Element of NAT st
for i being Element of NAT st K <= i holds
ex S2i being Division of ['c,b'] st
( S2i = T . i & 2 <= len S2i ) ) by A20; :: thesis: verum
end;
then consider PS2 being DivSequence of ['c,b'] such that
A25: ( delta PS2 is convergent & lim (delta PS2) = 0 ) and
A26: ex K being Element of NAT st
for i being Element of NAT st K <= i holds
ex S2i being Division of ['c,b'] st
( S2i = PS2 . i & 2 <= len S2i ) ;
consider K being Element of NAT such that
A27: for i being Element of NAT st K <= i holds
ex S2i being Division of ['c,b'] st
( S2i = PS2 . i & 2 <= len S2i ) by A26;
defpred S1[ set , set ] means ex n being Element of NAT ex e being Division of ['c,b'] st
( n = \$1 & e = \$2 & e = PS2 . (n + K) );
A28: for n being Element of NAT ex D being Element of divs ['c,b'] st S1[n,D]
proof
let n be Element of NAT ; :: thesis: ex D being Element of divs ['c,b'] st S1[n,D]
reconsider D = PS2 . (n + K) as Element of divs ['c,b'] by INTEGRA1:def 3;
take D ; :: thesis: S1[n,D]
thus S1[n,D] ; :: thesis: verum
end;
consider S2 being sequence of (divs ['c,b']) such that
A29: for n being Element of NAT holds S1[n,S2 . n] from reconsider S2 = S2 as DivSequence of ['c,b'] ;
defpred S2[ Element of NAT , set ] means ex S being Division of ['c,b'] st
( S = S2 . \$1 & \$2 = S /^ 1 );
A30: now :: thesis: for i being Element of NAT ex S2i being Division of ['c,b'] st
( S2i = S2 . i & 2 <= len S2i )
let i be Element of NAT ; :: thesis: ex S2i being Division of ['c,b'] st
( S2i = S2 . i & 2 <= len S2i )

ex n being Element of NAT ex e being Division of ['c,b'] st
( n = i & e = S2 . i & e = PS2 . (n + K) ) by A29;
hence ex S2i being Division of ['c,b'] st
( S2i = S2 . i & 2 <= len S2i ) by ; :: thesis: verum
end;
A31: for i being Element of NAT ex T being Element of divs ['c,b'] st S2[i,T]
proof
let i be Element of NAT ; :: thesis: ex T being Element of divs ['c,b'] st S2[i,T]
consider S being Division of ['c,b'] such that
A32: S = S2 . i and
A33: 2 <= len S by A30;
set T = S /^ 1;
A34: 1 <= len S by ;
2 - 1 <= (len S) - 1 by ;
then A35: 1 <= len (S /^ 1) by ;
then len (S /^ 1) in Seg (len (S /^ 1)) ;
then len (S /^ 1) in dom (S /^ 1) by FINSEQ_1:def 3;
then (S /^ 1) . (len (S /^ 1)) = S . ((len (S /^ 1)) + 1) by ;
then (S /^ 1) . (len (S /^ 1)) = S . (((len S) - 1) + 1) by ;
then A36: (S /^ 1) . (len (S /^ 1)) = upper_bound ['c,b'] by INTEGRA1:def 2;
( rng S c= ['c,b'] & rng (S /^ 1) c= rng S ) by ;
then A37: rng (S /^ 1) c= ['c,b'] ;
( not S /^ 1 is empty & S /^ 1 is increasing ) by ;
then S /^ 1 is Division of ['c,b'] by ;
then S /^ 1 is Element of divs ['c,b'] by INTEGRA1:def 3;
hence ex T being Element of divs ['c,b'] st S2[i,T] by A32; :: thesis: verum
end;
consider T2 being DivSequence of ['c,b'] such that
A38: for i being Element of NAT holds S2[i,T2 . i] from A39: for n being Element of NAT ex D being Division of ['c,b'] st
( D = T2 . n & ( for i being Element of NAT st i in dom D holds
c < D . i ) )
proof
let n be Element of NAT ; :: thesis: ex D being Division of ['c,b'] st
( D = T2 . n & ( for i being Element of NAT st i in dom D holds
c < D . i ) )

reconsider D = T2 . n as Division of ['c,b'] ;
take D ; :: thesis: ( D = T2 . n & ( for i being Element of NAT st i in dom D holds
c < D . i ) )

consider E being Division of ['c,b'] such that
A40: E = S2 . n and
A41: T2 . n = E /^ 1 by A38;
A42: ex E1 being Division of ['c,b'] st
( E1 = S2 . n & 2 <= len E1 ) by A30;
then A43: 2 - 1 <= (len E) - 1 by ;
A44: 1 <= len E by ;
then 1 in Seg (len E) ;
then A45: 1 in dom E by FINSEQ_1:def 3;
then ( rng E c= ['c,b'] & E . 1 in rng E ) by ;
then A46: c <= E . 1 by ;
2 in Seg (len E) by ;
then 2 in dom E by FINSEQ_1:def 3;
then A47: E . 1 < E . 2 by ;
len D = (len E) - 1 by ;
then 1 in Seg (len D) by A43;
then A48: 1 in dom D by FINSEQ_1:def 3;
then A49: D . 1 = E . (1 + 1) by ;
then A50: c < D . 1 by ;
now :: thesis: for i being Element of NAT st i in dom D holds
( ( i <> 1 implies c < D . i ) & c < D . i )
let i be Element of NAT ; :: thesis: ( i in dom D implies ( ( i <> 1 implies c < D . i ) & c < D . i ) )
assume A51: i in dom D ; :: thesis: ( ( i <> 1 implies c < D . i ) & c < D . i )
then A52: 1 <= i by FINSEQ_3:25;
hereby :: thesis: c < D . i
assume i <> 1 ; :: thesis: c < D . i
then 1 < i by ;
then D . 1 < D . i by ;
hence c < D . i by ; :: thesis: verum
end;
hence c < D . i by ; :: thesis: verum
end;
hence ( D = T2 . n & ( for i being Element of NAT st i in dom D holds
c < D . i ) ) ; :: thesis: verum
end;
set XAC = chi (['a,c'],['a,c']);
set XCB = chi (['c,b'],['c,b']);
consider T1 being DivSequence of ['a,c'] such that
A53: ( delta T1 is convergent & lim (delta T1) = 0 ) by INTEGRA4:11;
A54: for n being Element of NAT ex D being Division of ['c,b'] st
( D = T2 . n & 1 <= len D )
proof
let n be Element of NAT ; :: thesis: ex D being Division of ['c,b'] st
( D = T2 . n & 1 <= len D )

reconsider D = T2 . n as Division of ['c,b'] ;
take D ; :: thesis: ( D = T2 . n & 1 <= len D )
consider E being Division of ['c,b'] such that
A55: E = S2 . n and
A56: T2 . n = E /^ 1 by A38;
ex E1 being Division of ['c,b'] st
( E1 = S2 . n & 2 <= len E1 ) by A30;
then ( 1 <= len E & 2 - 1 <= (len E) - 1 ) by ;
hence ( D = T2 . n & 1 <= len D ) by ; :: thesis: verum
end;
A57: integral (f,c,b) = integral (f,['c,b']) by
.= integral (f || ['c,b']) ;
A58: integral (f,a,c) = integral (f,['a,c']) by ;
defpred S3[ Element of NAT , set ] means ex S1 being Division of ['a,c'] ex S2 being Division of ['c,b'] st
( S1 = T1 . \$1 & S2 = T2 . \$1 & \$2 = S1 ^ S2 );
A59: [.a,b.] = [.(),().] by ;
then A60: upper_bound ['a,b'] = b by ;
A61: for i being Element of NAT ex T being Element of divs ['a,b'] st S3[i,T]
proof
let i0 be Element of NAT ; :: thesis: ex T being Element of divs ['a,b'] st S3[i0,T]
reconsider S1 = T1 . i0 as Division of ['a,c'] ;
reconsider S2 = T2 . i0 as Division of ['c,b'] ;
set T = S1 ^ S2;
ex D being Division of ['c,b'] st
( D = T2 . i0 & 1 <= len D ) by A54;
then len S2 in Seg (len S2) ;
then A62: len S2 in dom S2 by FINSEQ_1:def 3;
A63: rng S1 c= ['a,c'] 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
A64: i in dom (S1 ^ S2) and
A65: j in dom (S1 ^ S2) and
A66: i < j ; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
A67: 1 <= i by ;
A68: j <= len (S1 ^ S2) by ;
A69: i <= len (S1 ^ S2) by ;
A70: now :: thesis: ( j > len S1 implies (S1 ^ S2) . i < (S1 ^ S2) . j )
j <= (len S1) + (len S2) by ;
then A71: j - (len S1) <= len S2 by XREAL_1:20;
assume A72: j > len S1 ; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
then A73: (S1 ^ S2) . j = S2 . (j - (len S1)) by ;
A74: (len S1) + 1 <= j by ;
then consider m being Nat such that
A75: ((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 A75;
then 1 <= 1 + m by ;
then 1 + m in Seg (len S2) by ;
then A76: j - (len S1) in dom S2 by ;
A77: now :: thesis: ( i > len S1 implies (S1 ^ S2) . i < (S1 ^ S2) . j )
i <= (len S1) + (len S2) by ;
then A78: i - (len S1) <= len S2 by XREAL_1:20;
A79: i - (len S1) < j - (len S1) by ;
assume A80: i > len S1 ; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
then A81: (len S1) + 1 <= i by NAT_1:13;
then consider m being Nat such that
A82: ((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 A82;
then 1 <= 1 + m by ;
then 1 + m in Seg (len S2) by ;
then A83: i - (len S1) in dom S2 by ;
(S1 ^ S2) . i = S2 . (i - (len S1)) by ;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by ; :: 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 A84: i in dom S1 by ;
then (S1 ^ S2) . i = S1 . i by FINSEQ_1:def 7;
then (S1 ^ S2) . i in rng S1 by ;
then A85: (S1 ^ S2) . i <= c by ;
ex DD being Division of ['c,b'] st
( DD = T2 . i0 & ( for k being Element of NAT st k in dom DD holds
c < DD . k ) ) by A39;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by ; :: thesis: verum
end;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A77; :: thesis: verum
end;
A86: 1 <= j by ;
now :: thesis: ( j <= len S1 implies (S1 ^ S2) . i < (S1 ^ S2) . j )
assume A87: j <= len S1 ; :: thesis: (S1 ^ S2) . i < (S1 ^ S2) . j
then A88: j in dom S1 by ;
then A89: (S1 ^ S2) . j = S1 . j by FINSEQ_1:def 7;
i <= len S1 by ;
then A90: i in dom S1 by ;
then (S1 ^ S2) . i = S1 . i by FINSEQ_1:def 7;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by ; :: thesis: verum
end;
hence (S1 ^ S2) . i < (S1 ^ S2) . j by A70; :: thesis: verum
end;
then A91: S1 ^ S2 is non empty increasing FinSequence of REAL by SEQM_3:def 1;
rng S2 c= ['c,b'] by INTEGRA1:def 2;
then (rng S1) \/ (rng S2) c= ['a,c'] \/ ['c,b'] by ;
then (rng S1) \/ (rng S2) c= [.a,b.] by ;
then A92: rng (S1 ^ S2) c= ['a,b'] by ;
(S1 ^ S2) . (len (S1 ^ S2)) = (S1 ^ S2) . ((len S1) + (len S2)) by FINSEQ_1:22
.= S2 . (len S2) by
.= upper_bound ['a,b'] by ;
then S1 ^ S2 is Division of ['a,b'] by ;
then S1 ^ S2 is Element of divs ['a,b'] by INTEGRA1:def 3;
hence ex T being Element of divs ['a,b'] st S3[i0,T] ; :: thesis: verum
end;
consider T being DivSequence of ['a,b'] such that
A93: for i being Element of NAT holds S3[i,T . i] from A94: lower_bound ['a,b'] = a by ;
A95: for i, k being Element of NAT
for S0 being Division of ['a,c'] 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,c'] st S0 = T1 . i & k in Seg (len S0) holds
divset ((T . i),k) = divset ((T1 . i),k)

let S0 be Division of ['a,c']; :: thesis: ( S0 = T1 . i & k in Seg (len S0) implies divset ((T . i),k) = divset ((T1 . i),k) )
assume A96: 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,b'] ;
A97: 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,c'], S2 being Division of ['c,b'] such that
A98: S1 = T1 . i and
S2 = T2 . i and
A99: T . i = S1 ^ S2 by A93;
assume A100: k in Seg (len S0) ; :: thesis: divset ((T . i),k) = divset ((T1 . i),k)
then A101: k in dom S1 by ;
len S = (len S1) + (len S2) by ;
then len S1 <= len S by NAT_1:11;
then Seg (len S1) c= Seg (len S) by FINSEQ_1:5;
then k in Seg (len S) by ;
then A102: k in dom S by FINSEQ_1:def 3;
A103: divset ((T . i),k) = [.(lower_bound (divset ((T . i),k))),(upper_bound (divset ((T . i),k))).] by INTEGRA1:4;
A104: now :: thesis: ( k <> 1 implies divset ((T . i),k) = divset ((T1 . i),k) )
( k <= len S1 & k - 1 <= k - 0 ) by ;
then A105: k - 1 <= len S1 by XXREAL_0:2;
assume A106: k <> 1 ; :: thesis: divset ((T . i),k) = divset ((T1 . i),k)
1 <= k by ;
then A107: 1 < k by ;
then 1 + 1 <= k by NAT_1:13;
then A108: 2 - 1 <= k - 1 by XREAL_1:9;
k - 1 is Element of NAT by ;
then k - 1 in Seg (len S1) by ;
then A109: 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
.= [.(S . (k - 1)),(S . k).] by
.= [.(S . (k - 1)),(S1 . k).] by
.= [.(S1 . (k - 1)),(S1 . k).] by
.= [.(lower_bound (divset ((T1 . i),k))),(S1 . k).] by
.= divset ((T1 . i),k) by ; :: thesis: verum
end;
now :: thesis: ( k = 1 implies divset ((T . i),k) = divset ((T1 . i),k) )
assume A110: k = 1 ; :: thesis: divset ((T . i),k) = divset ((T1 . i),k)
hence divset ((T . i),k) = [.(),(upper_bound (divset ((T . i),k))).] by
.= [.(),(S . k).] by
.= [.(),(S1 . k).] by
.= [.(lower_bound (divset ((T1 . i),k))),(S1 . 1).] by
.= divset ((T1 . i),k) by ;
:: thesis: verum
end;
hence divset ((T . i),k) = divset ((T1 . i),k) by A104; :: thesis: verum
end;
A111: upper_bound ['a,c'] = c by ;
A112: for i, k being Element of NAT
for S01 being Division of ['a,c']
for S02 being Division of ['c,b'] 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,c']
for S02 being Division of ['c,b'] 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,c']; :: thesis: for S02 being Division of ['c,b'] 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 ['c,b']; :: 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
A113: S01 = T1 . i and
A114: 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,b'] ;
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A115: S1 = T1 . i and
A116: S2 = T2 . i and
A117: T . i = S1 ^ S2 by A93;
assume A118: k in Seg (len S02) ; :: thesis: divset ((T . i),((len S01) + k)) = divset ((T2 . i),k)
then A119: k in dom S2 by ;
then A120: (len S1) + k in dom S by ;
A121: divset ((T2 . i),k) = [.(lower_bound (divset ((T2 . i),k))),(upper_bound (divset ((T2 . i),k))).] by INTEGRA1:4;
A122: 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;
A123: now :: thesis: ( k <> 1 implies divset ((T . i),((len S1) + k)) = divset ((T2 . i),k) )
( k <= len S2 & k - 1 <= k - 0 ) by ;
then A124: k - 1 <= len S2 by XXREAL_0:2;
assume A125: k <> 1 ; :: thesis: divset ((T . i),((len S1) + k)) = divset ((T2 . i),k)
A126: 1 <= k by ;
then A127: 1 < k by ;
then 1 + 1 <= k by NAT_1:13;
then A128: 2 - 1 <= k - 1 by XREAL_1:9;
k - 1 is Element of NAT by ;
then k - 1 in Seg (len S2) by ;
then A129: k - 1 in dom S2 by FINSEQ_1:def 3;
A130: 1 + 0 < k + (len S1) by ;
hence divset ((T . i),((len S1) + k)) = [.(S . (((len S1) + k) - 1)),(upper_bound (divset ((T . i),((len S1) + k)))).] by
.= [.(S . (((len S1) + k) - 1)),(S . ((len S1) + k)).] by
.= [.(S . ((len S1) + (k - 1))),(S2 . k).] by
.= [.(S2 . (k - 1)),(S2 . k).] by
.= [.(lower_bound (divset ((T2 . i),k))),(S2 . k).] by
.= divset ((T2 . i),k) by ;
:: 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 A131: len S1 in dom S1 by FINSEQ_1:def 3;
assume A132: k = 1 ; :: thesis: divset ((T . i),((len S1) + k)) = divset ((T2 . i),k)
len S1 <> 0 ;
then A133: (len S1) + k <> 1 by A132;
hence divset ((T . i),((len S1) + k)) = [.(S . (((len S1) + k) - 1)),(upper_bound (divset ((T . i),((len S1) + k)))).] by
.= [.(S1 . (len S1)),(upper_bound (divset ((T . i),((len S1) + k)))).] by
.= [.(),(upper_bound (divset ((T . i),((len S1) + k)))).] by INTEGRA1:def 2
.= [.(),(S . ((len S1) + k)).] by
.= [.(),(S2 . k).] by
.= [.(lower_bound (divset ((T2 . i),k))),(S2 . 1).] by
.= divset ((T2 . i),k) by ;
:: thesis: verum
end;
hence divset ((T . i),((len S01) + k)) = divset ((T2 . i),k) by ; :: thesis: verum
end;
set XAB = chi (['a,b'],['a,b']);
A134: for i, k being Element of NAT
for S0 being Division of ['c,b'] st S0 = T2 . i & k in Seg (len S0) holds
divset ((T2 . i),k) c= ['c,b']
proof
let i, k be Element of NAT ; :: thesis: for S0 being Division of ['c,b'] st S0 = T2 . i & k in Seg (len S0) holds
divset ((T2 . i),k) c= ['c,b']

let S0 be Division of ['c,b']; :: thesis: ( S0 = T2 . i & k in Seg (len S0) implies divset ((T2 . i),k) c= ['c,b'] )
assume that
A135: S0 = T2 . i and
A136: k in Seg (len S0) ; :: thesis: divset ((T2 . i),k) c= ['c,b']
k in dom S0 by ;
hence divset ((T2 . i),k) c= ['c,b'] by ; :: thesis: verum
end;
A137: ['a,c'] c= ['a,b'] by ;
then f | ['a,c'] is bounded by ;
then A138: (f || ['a,c']) | ['a,c'] is bounded ;
A139: for i, k being Element of NAT
for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds
divset ((T1 . i),k) c= ['a,c']
proof
let i, k be Element of NAT ; :: thesis: for S0 being Division of ['a,c'] st S0 = T1 . i & k in Seg (len S0) holds
divset ((T1 . i),k) c= ['a,c']

let S0 be Division of ['a,c']; :: thesis: ( S0 = T1 . i & k in Seg (len S0) implies divset ((T1 . i),k) c= ['a,c'] )
assume that
A140: S0 = T1 . i and
A141: k in Seg (len S0) ; :: thesis: divset ((T1 . i),k) c= ['a,c']
k in dom S0 by ;
hence divset ((T1 . i),k) c= ['a,c'] by ; :: thesis: verum
end;
A142: for i being Element of NAT holds upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i)))
proof
let i be Element of NAT ; :: thesis: upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i)))
reconsider F = upper_volume ((f || ['a,b']),(T . i)) as FinSequence of REAL ;
reconsider F1 = upper_volume ((f || ['a,c']),(T1 . i)) as FinSequence of REAL ;
reconsider F2 = upper_volume ((f || ['c,b']),(T2 . i)) as FinSequence of REAL ;
reconsider S = T . i as Division of ['a,b'] ;
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A143: S1 = T1 . i and
A144: S2 = T2 . i and
A145: T . i = S1 ^ S2 by A93;
A146: len F = len S by INTEGRA1:def 6
.= (len S1) + (len S2) by
.= (len F1) + (len S2) by
.= (len F1) + (len F2) by ;
A147: 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 A148: k in dom F2 ; :: thesis: F . ((len F1) + k) = F2 . k
then A149: k in Seg (len F2) by FINSEQ_1:def 3;
then 1 <= k by FINSEQ_1:1;
then A150: 1 + (len F1) <= k + (len F1) by XREAL_1:6;
k <= len F2 by ;
then A151: (len F1) + k <= len F by ;
1 <= 1 + (len F1) by NAT_1:11;
then 1 <= k + (len F1) by ;
then k + (len F1) in Seg (len F) by A151;
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 A152: F . ((len F1) + k) = (upper_bound (rng ((f || ['a,b']) | (divset ((T . i),((len F1) + k)))))) * (vol (divset ((T . i),((len F1) + k)))) by INTEGRA1:def 6;
k in Seg (len F2) by ;
then A153: k in Seg (len S2) by ;
then A154: k in dom S2 by FINSEQ_1:def 3;
len F1 = len S1 by ;
then A155: divset ((T . i),((len F1) + k)) = divset ((T2 . i),k) by ;
then A156: divset ((T . i),((len F1) + k)) c= ['c,b'] by ;
then divset ((T . i),((len F1) + k)) c= ['a,b'] by A17;
then F . ((len F1) + k) = (upper_bound (rng ((f || ['c,b']) | (divset ((T2 . i),k))))) * (vol (divset ((T2 . i),k))) by ;
hence F . ((len F1) + k) = F2 . k by ; :: thesis: verum
end;
A157: 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 A158: k in Seg (len F1) by FINSEQ_1:def 3;
then A159: k in Seg (len S1) by ;
then A160: k in dom S1 by FINSEQ_1:def 3;
len F1 <= len F by ;
then Seg (len F1) c= Seg (len F) by FINSEQ_1:5;
then k in Seg (len F) by A158;
then k in Seg (len S) by INTEGRA1:def 6;
then k in dom S by FINSEQ_1:def 3;
then A161: F . k = (upper_bound (rng ((f || ['a,b']) | (divset ((T . i),k))))) * (vol (divset ((T . i),k))) by INTEGRA1:def 6;
A162: divset ((T . i),k) = divset ((T1 . i),k) by ;
then A163: divset ((T . i),k) c= ['a,c'] by ;
then divset ((T . i),k) c= ['a,b'] by A137;
then F . k = (upper_bound (rng ((f || ['a,c']) | (divset ((T1 . i),k))))) * (vol (divset ((T1 . i),k))) by ;
hence F . k = F1 . k by ; :: thesis: verum
end;
dom F = Seg ((len F1) + (len F2)) by ;
hence upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i))) by ; :: thesis: verum
end;
A164: for i being Element of NAT holds Sum (upper_volume ((f || ['a,b']),(T . i))) = (Sum (upper_volume ((f || ['a,c']),(T1 . i)))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i))))
proof
let i be Element of NAT ; :: thesis: Sum (upper_volume ((f || ['a,b']),(T . i))) = (Sum (upper_volume ((f || ['a,c']),(T1 . i)))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i))))
upper_volume ((f || ['a,b']),(T . i)) = (upper_volume ((f || ['a,c']),(T1 . i))) ^ (upper_volume ((f || ['c,b']),(T2 . i))) by A142;
hence Sum (upper_volume ((f || ['a,b']),(T . i))) = (Sum (upper_volume ((f || ['a,c']),(T1 . i)))) + (Sum (upper_volume ((f || ['c,b']),(T2 . i)))) by RVSUM_1:75; :: thesis: verum
end;
now :: thesis: for i being Nat holds (upper_sum ((f || ['a,b']),T)) . i = ((upper_sum ((f || ['a,c']),T1)) . i) + ((upper_sum ((f || ['c,b']),T2)) . i)
let i be Nat; :: thesis: (upper_sum ((f || ['a,b']),T)) . i = ((upper_sum ((f || ['a,c']),T1)) . i) + ((upper_sum ((f || ['c,b']),T2)) . i)
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
thus (upper_sum ((f || ['a,b']),T)) . i = upper_sum ((f || ['a,b']),(T . ii)) by INTEGRA2:def 2
.= (upper_sum ((f || ['a,c']),(T1 . ii))) + (Sum (upper_volume ((f || ['c,b']),(T2 . ii)))) by A164
.= ((upper_sum ((f || ['a,c']),T1)) . i) + (upper_sum ((f || ['c,b']),(T2 . ii))) by INTEGRA2:def 2
.= ((upper_sum ((f || ['a,c']),T1)) . i) + ((upper_sum ((f || ['c,b']),T2)) . i) by INTEGRA2:def 2 ; :: thesis: verum
end;
then A165: upper_sum ((f || ['a,b']),T) = (upper_sum ((f || ['a,c']),T1)) + (upper_sum ((f || ['c,b']),T2)) by SEQ_1:7;
A166: f || ['c,b'] is Function of ['c,b'],REAL by ;
then A167: lower_integral (f || ['c,b']) <= upper_integral (f || ['c,b']) by ;
A168: 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
A169: for n being Nat st m <= n holds
|.(((delta PS2) . n) - 0).| < e by ;
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 )
A170: n <= n + K by NAT_1:11;
assume m <= n ; :: thesis: |.(((delta S2) . n) - 0).| < e
then m <= n + K by ;
then |.(((delta PS2) . (n + K)) - 0).| < e by A169;
then A171: |.((delta (PS2 . (n + K))) - 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 ['c,b'] st
( k = n & e1 = S2 . n & e1 = PS2 . (k + K) ) by A29;
hence |.(((delta S2) . n) - 0).| < e by ; :: thesis: verum
end;
end;
A172: 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 A173: 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
A174: for n being Nat st m <= n holds
|.(((delta S2) . n) - 0).| < e / 2 by ;
take m = m; :: thesis: for nn being Nat st m <= nn holds
|.(((delta T2) . nn) - 0).| < e

A175: e / 2 < e by ;
let nn be Nat; :: thesis: ( m <= nn implies |.(((delta T2) . nn) - 0).| < e )
assume A176: 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 ;
then ( 0 <= delta (S2 . n) & |.(delta (S2 . n)).| < e / 2 ) by ;
then A177: max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) < e / 2 by ABSVALUE:def 1;
A178: for y being Real st y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) holds
y < e
proof
reconsider D = T2 . n as Division of ['c,b'] ;
let y be Real; :: thesis: ( y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) implies y < e )
assume y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) ; :: thesis: y < e
then consider x being object such that
A179: x in dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) and
A180: y = (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) . x by FUNCT_1:def 3;
reconsider i = x as Element of NAT by A179;
A181: x in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) by ;
consider E1 being Division of ['c,b'] such that
A182: E1 = S2 . n and
A183: 2 <= len E1 by A30;
set i1 = i + 1;
consider E being Division of ['c,b'] such that
A184: E = S2 . n and
A185: T2 . n = E /^ 1 by A38;
A186: 1 <= len E1 by ;
then A187: len D = (len E) - 1 by ;
A188: len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) = len D by INTEGRA1:def 6;
then A189: dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) = dom D by FINSEQ_3:29;
A190: now :: thesis: ( i = 1 implies y < e )
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = len E by ;
then 2 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by ;
then 2 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def 3;
then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FUNCT_1:def 3;
then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by XXREAL_2:def 8;
then A191: (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2 < e / 2 by ;
assume A192: i = 1 ; :: thesis: y < e
then A193: 1 in dom D by ;
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len D) + 1 by ;
then len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) + 1 by INTEGRA1:def 6;
then 1 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by ;
then 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def 3;
then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FUNCT_1:def 3;
then (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by XXREAL_2:def 8;
then A194: (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1 < e / 2 by ;
A195: 2 in dom E by ;
1 in Seg (len E) by ;
then A196: 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 A197: divset ((S2 . n),1) = [.(),(upper_bound (divset ((S2 . n),1))).] by ;
then A198: [.(),(upper_bound (divset ((S2 . n),1))).] = [.(lower_bound [.(),(upper_bound (divset ((S2 . n),1))).]),(upper_bound [.(),(upper_bound (divset ((S2 . n),1))).]).] by INTEGRA1:4;
A199: divset ((T2 . n),i) = [.(lower_bound (divset ((T2 . n),1))),(upper_bound (divset ((T2 . n),1))).] by
.= [.(),(upper_bound (divset ((T2 . n),1))).] by
.= [.(),(D . 1).] by
.= [.(),(E . (1 + 1)).] by
.= [.(),(upper_bound (divset ((S2 . n),2))).] by ;
then [.(),(upper_bound (divset ((S2 . n),2))).] = [.(lower_bound [.(),(upper_bound (divset ((S2 . n),2))).]),(upper_bound [.(),(upper_bound (divset ((S2 . n),2))).]).] by INTEGRA1:4;
then A200: ( lower_bound ['c,b'] = lower_bound [.(),(upper_bound (divset ((S2 . n),2))).] & upper_bound (divset ((S2 . n),2)) = upper_bound [.(),(upper_bound (divset ((S2 . n),2))).] ) by ;
y = vol (divset ((T2 . n),1)) by ;
then y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + ((upper_bound [.(),(upper_bound (divset ((S2 . n),1))).]) - ()) by ;
then A201: y = ((upper_bound (divset ((S2 . n),2))) - (upper_bound (divset ((S2 . n),1)))) + (vol (divset ((S2 . n),1))) by ;
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 ;
then A202: divset ((S2 . n),2) = [.(upper_bound (divset ((S2 . n),1))),(upper_bound (divset ((S2 . n),2))).] by ;
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 = (vol (divset ((S2 . n),2))) + (vol (divset ((S2 . n),1))) by ;
then y = ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2) + (vol (divset ((S2 . n),1))) by ;
then y = ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 2) + ((upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . 1) by ;
then y < (e / 2) + (e / 2) by ;
hence y < e ; :: thesis: verum
end;
A203: y = (upper_bound (rng ((chi (['c,b'],['c,b'])) | (divset ((T2 . n),i))))) * (vol (divset ((T2 . n),i))) by ;
now :: thesis: ( i <> 1 implies y < e )
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len D) + 1 by ;
then len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = (len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) + 1 by INTEGRA1:def 6;
then A204: i + 1 in Seg (len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by ;
then A205: i + 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by FINSEQ_1:def 3;
A206: i + 1 in dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by ;
A207: i in dom D by ;
Seg ((len D) + 1) = Seg (len E) by A187;
then i + 1 in Seg (len E) by ;
then A208: i + 1 in dom E by FINSEQ_1:def 3;
len (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = len E by ;
then A209: dom (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) = dom E by FINSEQ_3:29;
assume A210: i <> 1 ; :: thesis: y < e
i in Seg (len D) by ;
then 1 <= i by FINSEQ_1:1;
then A211: 1 < i by ;
then A212: i - 1 in Seg (len D) by ;
then A213: i - 1 in dom D by FINSEQ_1:def 3;
reconsider i9 = i - 1 as Element of NAT by A212;
1 + 1 < i + 1 by ;
then A214: 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
.= [.(D . (i - 1)),(D . i).] by
.= [.(E . (i9 + 1)),(D . i).] by
.= [.(E . ((i - 1) + 1)),(E . (i + 1)).] by
.= [.(E . ((i + 1) - 1)),(upper_bound (divset ((S2 . n),(i + 1)))).] by
.= [.(lower_bound (divset ((S2 . n),(i + 1)))),(upper_bound (divset ((S2 . n),(i + 1)))).] by
.= divset ((S2 . n),(i + 1)) by INTEGRA1:4 ;
then y = (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) . (i + 1) by ;
then y in rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n))) by ;
then y <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(S2 . n)))) by XXREAL_2:def 8;
then y < e / 2 by ;
hence y < e by ; :: thesis: verum
end;
hence y < e by A190; :: thesis: verum
end;
max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n)))) in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . n))) by XXREAL_2:def 8;
then ( 0 <= delta (T2 . n) & delta (T2 . n) < e ) by ;
then |.(delta (T2 . n)).| < e by ABSVALUE:def 1;
hence |.(((delta T2) . nn) - 0).| < e by INTEGRA3:def 2; :: thesis: verum
end;
then A215: delta T2 is convergent by SEQ_2:def 6;
then A216: lim (delta T2) = 0 by ;
then A217: ( upper_sum ((f || ['c,b']),T2) is convergent & lim (upper_sum ((f || ['c,b']),T2)) = upper_integral (f || ['c,b']) ) by ;
A218: now :: thesis: for e being Real st 0 < e holds
ex n being Nat st
for mm being Nat st n <= mm holds
|.((() . mm) - 0).| < e
let e be Real; :: thesis: ( 0 < e implies ex n being Nat st
for mm being Nat st n <= mm holds
|.((() . mm) - 0).| < e )

assume A219: 0 < e ; :: thesis: ex n being Nat st
for mm being Nat st n <= mm holds
|.((() . mm) - 0).| < e

then consider n1 being Nat such that
A220: for m being Nat st n1 <= m holds
|.(((delta T1) . m) - 0).| < e by ;
consider n2 being Nat such that
A221: for m being Nat st n2 <= m holds
|.(((delta T2) . m) - 0).| < e by ;
reconsider n = max (n1,n2) as Nat by TARSKI:1;
take n = n; :: thesis: for mm being Nat st n <= mm holds
|.((() . mm) - 0).| < e

let mm be Nat; :: thesis: ( n <= mm implies |.((() . mm) - 0).| < e )
assume A222: n <= mm ; :: thesis: |.((() . mm) - 0).| < e
reconsider m = mm as Element of NAT by ORDINAL1:def 12;
n2 <= n by XXREAL_0:25;
then n2 <= m by ;
then |.(((delta T2) . m) - 0).| < e by A221;
then A223: |.(delta (T2 . m)).| < e by INTEGRA3:def 2;
0 <= delta (T2 . m) by INTEGRA3:9;
then A224: max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m)))) < e by ;
n1 <= n by XXREAL_0:25;
then n1 <= m by ;
then |.(((delta T1) . m) - 0).| < e by A220;
then A225: |.(delta (T1 . m)).| < e by INTEGRA3:def 2;
0 <= delta (T1 . m) by INTEGRA3:9;
then A226: max (rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m)))) < e by ;
A227: for r being Real st r in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) holds
r < e
proof
reconsider Tm = T . m as Division of ['a,b'] ;
let y be Real; :: thesis: ( y in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) implies y < e )
assume y in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) ; :: thesis: y < e
then consider x being object such that
A228: x in dom (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) and
A229: y = (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) . x by FUNCT_1:def 3;
reconsider i = x as Element of NAT by A228;
A230: x in Seg (len (upper_volume ((chi (['a,b'],['a,b'])),(T . m)))) by ;
then A231: 1 <= i by FINSEQ_1:1;
A232: len (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) = len Tm by INTEGRA1:def 6;
then A233: i <= len Tm by ;
dom (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) = dom Tm by ;
then A234: y = (upper_bound (rng ((chi (['a,b'],['a,b'])) | (divset ((T . m),i))))) * (vol (divset ((T . m),i))) by ;
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A235: S1 = T1 . m and
A236: S2 = T2 . m and
A237: T . m = S1 ^ S2 by A93;
A238: len Tm = (len S1) + (len S2) by ;
per cases ( i <= len S1 or i > len S1 ) ;
suppose i <= len S1 ; :: thesis: y < e
then A239: i in Seg (len S1) by A231;
then A240: i in dom S1 by FINSEQ_1:def 3;
len (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) = len S1 by ;
then A241: i in dom (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) by ;
A242: divset ((T1 . m),i) = divset ((T . m),i) by ;
A243: divset ((T1 . m),i) c= ['a,c'] by ;
then divset ((T1 . m),i) c= ['a,b'] by A137;
then (chi (['a,c'],['a,c'])) | (divset ((T1 . m),i)) = (chi (['a,b'],['a,b'])) | (divset ((T . m),i)) by ;
then y = (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) . i by ;
then y in rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m))) by ;
then y <= max (rng (upper_volume ((chi (['a,c'],['a,c'])),(T1 . m)))) by XXREAL_2:def 8;
hence y < e by ; :: thesis: verum
end;
suppose i > len S1 ; :: thesis: y < e
then A244: (len S1) + 1 <= i by NAT_1:13;
then consider k being Nat such that
A245: ((len S1) + 1) + k = i by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
set i1 = 1 + k;
A246: i - (len S1) <= len S2 by ;
1 + k = i - (len S1) by A245;
then 1 <= 1 + k by ;
then A247: 1 + k in Seg (len S2) by ;
then A248: 1 + k in dom S2 by FINSEQ_1:def 3;
A249: divset ((T2 . m),(1 + k)) = divset ((T . m),((len S1) + (1 + k))) by ;
A250: divset ((T2 . m),(1 + k)) c= ['c,b'] by ;
then divset ((T2 . m),(1 + k)) c= ['a,b'] by A17;
then y = (upper_bound (rng ((chi (['c,b'],['c,b'])) | (divset ((T2 . m),(1 + k)))))) * (vol (divset ((T2 . m),(1 + k)))) by ;
then A251: y = (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) . (1 + k) by ;
len (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) = len S2 by ;
then 1 + k in dom (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) by ;
then y in rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m))) by ;
then y <= max (rng (upper_volume ((chi (['c,b'],['c,b'])),(T2 . m)))) by XXREAL_2:def 8;
hence y < e by ; :: thesis: verum
end;
end;
end;
A252: 0 <= delta (T . m) by INTEGRA3:9;
max (rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m)))) in rng (upper_volume ((chi (['a,b'],['a,b'])),(T . m))) by XXREAL_2:def 8;
then delta (T . m) < e by A227;
then |.(delta (T . m)).| < e by ;
hence |.((() . mm) - 0).| < e by INTEGRA3:def 2; :: thesis: verum
end;
then A253: delta T is convergent by SEQ_2:def 6;
then A254: lim () = 0 by ;
(f || ['a,b']) | ['a,b'] is bounded by A4;
then A255: upper_integral (f || ['a,b']) = lim (upper_sum ((f || ['a,b']),T)) by ;
A256: for i being Element of NAT holds lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i)))
proof
let i be Element of NAT ; :: thesis: lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i)))
reconsider F = lower_volume ((f || ['a,b']),(T . i)) as FinSequence of REAL ;
reconsider F1 = lower_volume ((f || ['a,c']),(T1 . i)) as FinSequence of REAL ;
reconsider F2 = lower_volume ((f || ['c,b']),(T2 . i)) as FinSequence of REAL ;
reconsider S = T . i as Division of ['a,b'] ;
consider S1 being Division of ['a,c'], S2 being Division of ['c,b'] such that
A257: S1 = T1 . i and
A258: S2 = T2 . i and
A259: T . i = S1 ^ S2 by A93;
A260: len F = len S by INTEGRA1:def 7
.= (len S1) + (len S2) by
.= (len F1) + (len S2) by ;
then A261: len F = (len F1) + (len F2) by ;
A262: 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 A263: k in Seg (len F2) by FINSEQ_1:def 3;
then 1 <= k by FINSEQ_1:1;
then A264: 1 + (len F1) <= k + (len F1) by XREAL_1:6;
k <= len F2 by ;
then A265: (len F1) + k <= len F by ;
1 <= 1 + (len F1) by NAT_1:11;
then 1 <= k + (len F1) by ;
then k + (len F1) in Seg (len F) by A265;
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 A266: F . ((len F1) + k) = (lower_bound (rng ((f || ['a,b']) | (divset ((T . i),((len F1) + k)))))) * (vol (divset ((T . i),((len F1) + k)))) by INTEGRA1:def 7;
A267: k in Seg (len S2) by ;
then A268: k in dom S2 by FINSEQ_1:def 3;
len F1 = len S1 by ;
then A269: divset ((T . i),((len F1) + k)) = divset ((T2 . i),k) by ;
A270: divset ((T2 . i),k) c= ['c,b'] by ;
then divset ((T . i),((len F1) + k)) c= ['a,b'] by ;
then F . ((len F1) + k) = (lower_bound (rng ((f || ['c,b']) | (divset ((T2 . i),k))))) * (vol (divset ((T2 . i),k))) by ;
hence F . ((len F1) + k) = F2 . k by ; :: thesis: verum
end;
A271: 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,b']),(T . i))) = len S by INTEGRA1:def 7;
then A272: dom (lower_volume ((f || ['a,b']),(T . i))) = dom S by FINSEQ_3:29;
assume A273: k in dom F1 ; :: thesis: F . k = F1 . k
then k in Seg (len F1) by FINSEQ_1:def 3;
then A274: k in Seg (len S1) by ;
then A275: k in dom S1 by FINSEQ_1:def 3;
len F1 <= len F by ;
then dom F1 c= dom F by FINSEQ_3:30;
then A276: F . k = (lower_bound (rng ((f || ['a,b']) | (divset ((T . i),k))))) * (vol (divset ((T . i),k))) by ;
A277: ( divset ((T . i),k) = divset ((T1 . i),k) & divset ((T1 . i),k) c= ['a,c'] ) by ;
then divset ((T . i),k) c= ['a,b'] by A137;
then F . k = (lower_bound (rng ((f || ['a,c']) | (divset ((T1 . i),k))))) * (vol (divset ((T1 . i),k))) by ;
hence F . k = F1 . k by ; :: thesis: verum
end;
dom F = Seg ((len F1) + (len F2)) by ;
hence lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i))) by ; :: thesis: verum
end;
A278: for i being Element of NAT holds Sum (lower_volume ((f || ['a,b']),(T . i))) = (Sum (lower_volume ((f || ['a,c']),(T1 . i)))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i))))
proof
let i be Element of NAT ; :: thesis: Sum (lower_volume ((f || ['a,b']),(T . i))) = (Sum (lower_volume ((f || ['a,c']),(T1 . i)))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i))))
lower_volume ((f || ['a,b']),(T . i)) = (lower_volume ((f || ['a,c']),(T1 . i))) ^ (lower_volume ((f || ['c,b']),(T2 . i))) by A256;
hence Sum (lower_volume ((f || ['a,b']),(T . i))) = (Sum (lower_volume ((f || ['a,c']),(T1 . i)))) + (Sum (lower_volume ((f || ['c,b']),(T2 . i)))) by RVSUM_1:75; :: thesis: verum
end;
now :: thesis: for i being Nat holds (lower_sum ((f || ['a,b']),T)) . i = ((lower_sum ((f || ['a,c']),T1)) . i) + ((lower_sum ((f || ['c,b']),T2)) . i)
let i be Nat; :: thesis: (lower_sum ((f || ['a,b']),T)) . i = ((lower_sum ((f || ['a,c']),T1)) . i) + ((lower_sum ((f || ['c,b']),T2)) . i)
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
thus (lower_sum ((f || ['a,b']),T)) . i = lower_sum ((f || ['a,b']),(T . ii)) by INTEGRA2:def 3
.= (lower_sum ((f || ['a,c']),(T1 . ii))) + (Sum (lower_volume ((f || ['c,b']),(T2 . ii)))) by A278
.= ((lower_sum ((f || ['a,c']),T1)) . i) + (lower_sum ((f || ['c,b']),(T2 . ii))) by INTEGRA2:def 3
.= ((lower_sum ((f || ['a,c']),T1)) . i) + ((lower_sum ((f || ['c,b']),T2)) . i) by INTEGRA2:def 3 ; :: thesis: verum
end;
then A279: lower_sum ((f || ['a,b']),T) = (lower_sum ((f || ['a,c']),T1)) + (lower_sum ((f || ['c,b']),T2)) by SEQ_1:7;
A280: f || ['a,c'] is Function of ['a,c'],REAL by ;
then A281: ( f || ['a,c'] is upper_integrable & f || ['a,c'] is lower_integrable ) by ;
A282: ( upper_sum ((f || ['a,c']),T1) is convergent & lim (upper_sum ((f || ['a,c']),T1)) = upper_integral (f || ['a,c']) ) by ;
then A283: (upper_integral (f || ['a,c'])) + (upper_integral (f || ['c,b'])) = upper_integral (f || ['a,b']) by ;
A284: ( lower_sum ((f || ['a,c']),T1) is convergent & lim (lower_sum ((f || ['a,c']),T1)) = lower_integral (f || ['a,c']) ) by ;
(f || ['a,b']) | ['a,b'] is bounded by A4;
then A285: lower_integral (f || ['a,b']) = lim (lower_sum ((f || ['a,b']),T)) by ;
( lower_sum ((f || ['c,b']),T2) is convergent & lim (lower_sum ((f || ['c,b']),T2)) = lower_integral (f || ['c,b']) ) by ;
then A286: (lower_integral (f || ['a,c'])) + (lower_integral (f || ['c,b'])) = lower_integral (f || ['a,b']) by ;
integral (f,a,b) = integral (f,['a,b']) by
.= (integral (f || ['a,c'])) + (integral (f || ['c,b'])) by ;
hence integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) by ; :: thesis: ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )
f || ['a,b'] is integrable by A3;
then A287: upper_integral (f || ['a,b']) = lower_integral (f || ['a,b']) ;
A288: ( f || ['c,b'] is upper_integrable & f || ['c,b'] is lower_integrable ) by ;
A289: lower_integral (f || ['a,c']) <= upper_integral (f || ['a,c']) by ;
then lower_integral (f || ['c,b']) = upper_integral (f || ['c,b']) by ;
then A290: f || ['c,b'] is integrable by A288;
lower_integral (f || ['a,c']) = upper_integral (f || ['a,c']) by ;
then f || ['a,c'] is integrable by A281;
hence ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) by A290; :: thesis: verum